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  2485  reubida  2672  rmobida  2677  mpteq12f  4101  reuhypd  4492  funbrfv2b  5584  dffn5im  5585  eqfnfv2  5638  fndmin  5647  fniniseg  5660  rexsupp  5664  fmptco  5706  dff13  5793  riotabidva  5872  mpoeq123dva  5961  mpoeq3dva  5964  mpoxopovel  6270  qliftfun  6647  erovlem  6657  xpcomco  6856  pw2f1odclem  6866  elfi2  7005  ctssdccl  7144  ltexpi  7371  dfplpq2  7388  axprecex  7914  zrevaddcl  9338  qrevaddcl  9680  icoshft  10026  fznn  10125  shftdm  10872  2shfti  10881  sumeq2  11408  fsum3  11436  fsum2dlemstep  11483  prodeq2  11606  fprodseq  11632  gcdaddm  12026  grpidpropdg  12861  ismgmid  12864  gsumpropd2  12879  mhmpropd  12941  issubm2  12948  eqgid  13190  eqgabl  13292  rngpropd  13334  iscrng2  13394  ringpropd  13417  crngpropd  13418  crngunit  13486  dvdsrpropdg  13522  issubrg3  13619  lsslss  13722  lsspropdg  13772  bastop2  14069  restopn2  14168  iscnp3  14188  lmbr2  14199  txlm  14264  ismet2  14339  xblpnfps  14383  xblpnf  14384  blininf  14409  blres  14419  elmopn2  14434  neibl  14476  metrest  14491  metcnp3  14496  metcnp  14497  metcnp2  14498  metcn  14499  txmetcn  14504  cnbl0  14519  cnblcld  14520  bl2ioo  14527  elcncf2  14546  cncfmet  14564  cnlimc  14626