MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  hban Unicode version

Theorem hban 1846
Description: If  x is not free in  ph and  ps, it is not free in  ( ph  /\  ps ). (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 2-Jan-2018.)
Hypotheses
Ref Expression
hb.1  |-  ( ph  ->  A. x ph )
hb.2  |-  ( ps 
->  A. x ps )
Assertion
Ref Expression
hban  |-  ( (
ph  /\  ps )  ->  A. x ( ph  /\ 
ps ) )

Proof of Theorem hban
StepHypRef Expression
1 hb.1 . . . 4  |-  ( ph  ->  A. x ph )
21nfi 1557 . . 3  |-  F/ x ph
3 hb.2 . . . 4  |-  ( ps 
->  A. x ps )
43nfi 1557 . . 3  |-  F/ x ps
52, 4nfan 1842 . 2  |-  F/ x
( ph  /\  ps )
65nfri 1774 1  |-  ( (
ph  /\  ps )  ->  A. x ( ph  /\ 
ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359   A.wal 1546
This theorem is referenced by:  hb3anOLD  1849  dvelimvOLD  1994  dvelimhOLD  2018  dvelimALT  2191  dvelimf-o  2238  ax11indalem  2255  ax11inda2ALT  2256  cleqh  2509  hbimpg  28360  hbimpgVD  28734  bnj982  28867  bnj1351  28916  bnj1352  28917  bnj1441  28930  dvelimvNEW7  29180  dvelimhvAUX7  29210  dvelimALTNEW7  29349  dvelimhOLD7  29409
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-11 1757
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1548  df-nf 1551
  Copyright terms: Public domain W3C validator