Theorem pm5.32da 456

Description: Distribution of implication over biconditional (deduction form). (Contributed by NM, 9-Dec-2006.)

Hypothesis

Ref	Expression
pm5.32da.1	|- ( ( ph /\ ps ) -> ( ch <-> th ) )

Assertion

Ref	Expression
pm5.32da	|- ( ph -> ( ( ps /\ ch ) <-> ( ps /\ th ) ) )

Proof of Theorem pm5.32da

Step	Hyp	Ref	Expression
1		pm5.32da.1	. . 3 |- ( ( ph /\ ps ) -> ( ch <-> th ) )
2	1	ex 115	. 2 |- ( ph -> ( ps -> ( ch <-> th ) ) )
3	2	pm5.32d 454	1 |- ( ph -> ( ( ps /\ ch ) <-> ( ps /\ th ) ) )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   <-> wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  rexbida  2545  reubida  2734  rmobida  2740  mpteq12f  4211  reuhypd  4617  funbrfv2b  5747  dffn5im  5748  eqfnfv2  5807  fndmin  5816  fniniseg  5829  fmptco  5874  dff13  5974  riotabidva  6056  mpoeq123dva  6149  mpoeq3dva  6152  suppssrst  6501  suppssrgst  6502  mpoxopovel  6512  qliftfun  6891  erovlem  6901  mapsnend  7099  xpcomco  7124  pw2f1odclem  7134  elfi2  7306  ctssdccl  7451  ltexpi  7704  dfplpq2  7721  axprecex  8247  zrevaddcl  9695  qrevaddcl  10044  icoshft  10392  fznn  10496  sseqn  11279  pfxeq  11468  pfxsuffeqwrdeq  11470  pfxsuff1eqwrdeq  11471  shftdm  11587  2shfti  11596  sumeq2  12125  fsum3  12154  fsum2dlemstep  12201  prodeq2  12324  fprodseq  12350  bitsmod  12723  bitscmp  12725  gcdaddm  12761  grpidpropdg  13694  ismgmid  13697  mhmpropd  13773  issubm2  13780  eqgid  14029  eqgabl  14134  rngpropd  14254  iscrng2  14319  ringpropd  14343  crngpropd  14344  crngunit  14418  dvdsrpropdg  14454  issubrg3  14555  lsslss  14718  lsspropdg  14768  znleval  14988  bastop2  15185  restopn2  15284  iscnp3  15304  lmbr2  15315  txlm  15380  ismet2  15455  xblpnfps  15499  xblpnf  15500  blininf  15525  blres  15535  elmopn2  15550  neibl  15592  metrest  15607  metcnp3  15612  metcnp  15613  metcnp2  15614  metcn  15615  txmetcn  15620  cnbl0  15635  cnblcld  15636  bl2ioo  15651  elcncf2  15675  cncfmet  15693  cnlimc  15773  lgsquadlem1  16196  lgsquadlem2  16197  2lgslem1a  16207  upgriswlkdc  16601  isclwwlknx  16657  clwwlkn1  16659  clwwlkn2  16662  eupth2lemsfi  16719