Theorem pm5.32da 452

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 450	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  2489  reubida  2676  rmobida  2681  mpteq12f  4109  reuhypd  4502  funbrfv2b  5601  dffn5im  5602  eqfnfv2  5656  fndmin  5665  fniniseg  5678  rexsupp  5682  fmptco  5724  dff13  5811  riotabidva  5890  mpoeq123dva  5979  mpoeq3dva  5982  mpoxopovel  6294  qliftfun  6671  erovlem  6681  xpcomco  6880  pw2f1odclem  6890  elfi2  7031  ctssdccl  7170  ltexpi  7397  dfplpq2  7414  axprecex  7940  zrevaddcl  9367  qrevaddcl  9709  icoshft  10056  fznn  10155  shftdm  10966  2shfti  10975  sumeq2  11502  fsum3  11530  fsum2dlemstep  11577  prodeq2  11700  fprodseq  11726  gcdaddm  12121  grpidpropdg  12957  ismgmid  12960  gsumpropd2  12976  mhmpropd  13038  issubm2  13045  eqgid  13296  eqgabl  13400  rngpropd  13451  iscrng2  13511  ringpropd  13534  crngpropd  13535  crngunit  13607  dvdsrpropdg  13643  issubrg3  13743  lsslss  13877  lsspropdg  13927  znleval  14141  bastop2  14252  restopn2  14351  iscnp3  14371  lmbr2  14382  txlm  14447  ismet2  14522  xblpnfps  14566  xblpnf  14567  blininf  14592  blres  14602  elmopn2  14617  neibl  14659  metrest  14674  metcnp3  14679  metcnp  14680  metcnp2  14681  metcn  14682  txmetcn  14687  cnbl0  14702  cnblcld  14703  bl2ioo  14710  elcncf2  14729  cncfmet  14747  cnlimc  14826  lgsquadlem1  15191