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 ) ) )

Syntax hints:   -> wi 4   /\ wa 104   <-> wb 105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  rexbida  2545  reubida  2734  rmobida  2740  mpteq12f  4206  reuhypd  4612  funbrfv2b  5741  dffn5im  5742  eqfnfv2  5798  fndmin  5807  fniniseg  5820  fmptco  5865  dff13  5964  riotabidva  6046  mpoeq123dva  6139  mpoeq3dva  6142  suppssrst  6491  suppssrgst  6492  mpoxopovel  6502  qliftfun  6881  erovlem  6891  mapsnend  7089  xpcomco  7114  pw2f1odclem  7124  elfi2  7296  ctssdccl  7441  ltexpi  7694  dfplpq2  7711  axprecex  8237  zrevaddcl  9674  qrevaddcl  10023  icoshft  10371  fznn  10474  sseqn  11257  pfxeq  11446  pfxsuffeqwrdeq  11448  pfxsuff1eqwrdeq  11449  shftdm  11565  2shfti  11574  sumeq2  12103  fsum3  12132  fsum2dlemstep  12179  prodeq2  12302  fprodseq  12328  bitsmod  12701  bitscmp  12703  gcdaddm  12739  grpidpropdg  13671  ismgmid  13674  mhmpropd  13750  issubm2  13757  eqgid  14006  eqgabl  14111  rngpropd  14229  iscrng2  14293  ringpropd  14316  crngpropd  14317  crngunit  14391  dvdsrpropdg  14427  issubrg3  14528  lsslss  14690  lsspropdg  14740  znleval  14960  bastop2  15108  restopn2  15207  iscnp3  15227  lmbr2  15238  txlm  15303  ismet2  15378  xblpnfps  15422  xblpnf  15423  blininf  15448  blres  15458  elmopn2  15473  neibl  15515  metrest  15530  metcnp3  15535  metcnp  15536  metcnp2  15537  metcn  15538  txmetcn  15543  cnbl0  15558  cnblcld  15559  bl2ioo  15574  elcncf2  15598  cncfmet  15616  cnlimc  15696  lgsquadlem1  16110  lgsquadlem2  16111  2lgslem1a  16121  upgriswlkdc  16515  isclwwlknx  16571  clwwlkn1  16573  clwwlkn2  16576  eupth2lemsfi  16633