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  2527  reubida  2715  rmobida  2721  mpteq12f  4169  reuhypd  4568  funbrfv2b  5690  dffn5im  5691  eqfnfv2  5745  fndmin  5754  fniniseg  5767  rexsupp  5771  fmptco  5813  dff13  5908  riotabidva  5988  mpoeq123dva  6081  mpoeq3dva  6084  mpoxopovel  6406  qliftfun  6785  erovlem  6795  xpcomco  7009  pw2f1odclem  7019  elfi2  7170  ctssdccl  7309  ltexpi  7556  dfplpq2  7573  axprecex  8099  zrevaddcl  9529  qrevaddcl  9877  icoshft  10224  fznn  10323  pfxeq  11276  pfxsuffeqwrdeq  11278  pfxsuff1eqwrdeq  11279  shftdm  11382  2shfti  11391  sumeq2  11919  fsum3  11947  fsum2dlemstep  11994  prodeq2  12117  fprodseq  12143  bitsmod  12516  bitscmp  12518  gcdaddm  12554  grpidpropdg  13456  ismgmid  13459  gsumpropd2  13475  mhmpropd  13548  issubm2  13555  eqgid  13812  eqgabl  13916  rngpropd  13967  iscrng2  14027  ringpropd  14050  crngpropd  14051  crngunit  14124  dvdsrpropdg  14160  issubrg3  14260  lsslss  14394  lsspropdg  14444  znleval  14666  bastop2  14807  restopn2  14906  iscnp3  14926  lmbr2  14937  txlm  15002  ismet2  15077  xblpnfps  15121  xblpnf  15122  blininf  15147  blres  15157  elmopn2  15172  neibl  15214  metrest  15229  metcnp3  15234  metcnp  15235  metcnp2  15236  metcn  15237  txmetcn  15242  cnbl0  15257  cnblcld  15258  bl2ioo  15273  elcncf2  15297  cncfmet  15315  cnlimc  15395  lgsquadlem1  15805  lgsquadlem2  15806  2lgslem1a  15816  upgriswlkdc  16210  isclwwlknx  16266  clwwlkn1  16268  clwwlkn2  16271