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

Theorem hban 1851
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 1561 . . 3  |-  F/ x ph
3 hb.2 . . . 4  |-  ( ps 
->  A. x ps )
43nfi 1561 . . 3  |-  F/ x ps
52, 4nfan 1847 . 2  |-  F/ x
( ph  /\  ps )
65nfri 1779 1  |-  ( (
ph  /\  ps )  ->  A. x ( ph  /\ 
ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360   A.wal 1550
This theorem is referenced by:  hb3anOLD  1854  dvelimvOLD  2029  dvelimhOLD  2073  dvelimALT  2212  dvelimf-o  2259  ax11indalem  2276  ax11inda2ALT  2277  cleqh  2535  hbimpg  28715  hbimpgVD  29090  bnj982  29223  bnj1351  29272  bnj1352  29273  bnj1441  29286  dvelimvNEW7  29536  dvelimhvAUX7  29566  dvelimALTNEW7  29710  dvelimhOLD7  29787
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-11 1762
This theorem depends on definitions:  df-bi 179  df-an 362  df-ex 1552  df-nf 1555
  Copyright terms: Public domain W3C validator