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  7452  ltexpi  7705  dfplpq2  7722  axprecex  8248  zrevaddcl  9700  qrevaddcl  10054  icoshft  10403  fznn  10507  sseqn  11295  pfxeq  11484  pfxsuffeqwrdeq  11486  pfxsuff1eqwrdeq  11487  shftdm  11603  2shfti  11612  sumeq2  12144  fsum3  12173  fsum2dlemstep  12220  prodeq2  12343  fprodseq  12369  bitsmod  12742  bitscmp  12744  gcdaddm  12780  grpidpropdg  13747  ismgmid  13750  mhmpropd  13826  issubm2  13833  eqgid  14082  eqgabl  14218  rngpropd  14338  iscrng2  14403  ringpropd  14427  crngpropd  14428  crngunit  14502  dvdsrpropdg  14538  issubrg3  14639  lsslss  14802  lsspropdg  14852  znleval  15072  bastop2  15276  restopn2  15375  iscnp3  15395  lmbr2  15406  txlm  15471  ismet2  15546  xblpnfps  15590  xblpnf  15591  blininf  15616  blres  15626  elmopn2  15641  neibl  15683  metrest  15698  metcnp3  15703  metcnp  15704  metcnp2  15705  metcn  15706  txmetcn  15711  cnbl0  15726  cnblcld  15727  bl2ioo  15742  elcncf2  15766  cncfmet  15784  cnlimc  15864  lgsquadlem1  16362  lgsquadlem2  16363  2lgslem1a  16373  upgriswlkdc  16767  isclwwlknx  16823  clwwlkn1  16825  clwwlkn2  16828  eupth2lemsfi  16885