Theorem pm5.32da 448

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 114	. 2 |- ( ph -> ( ps -> ( ch <-> th ) ) )
3	2	pm5.32d 446	1 |- ( ph -> ( ( ps /\ ch ) <-> ( ps /\ th ) ) )

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

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  rexbida  2459  reubida  2645  rmobida  2650  mpteq12f  4056  reuhypd  4443  funbrfv2b  5525  dffn5im  5526  eqfnfv2  5578  fndmin  5586  fniniseg  5599  rexsupp  5603  fmptco  5645  dff13  5730  riotabidva  5808  mpoeq123dva  5894  mpoeq3dva  5897  mpoxopovel  6200  qliftfun  6574  erovlem  6584  xpcomco  6783  elfi2  6928  ctssdccl  7067  ltexpi  7269  dfplpq2  7286  axprecex  7812  zrevaddcl  9232  qrevaddcl  9573  icoshft  9917  fznn  10014  shftdm  10750  2shfti  10759  sumeq2  11286  fsum3  11314  fsum2dlemstep  11361  prodeq2  11484  fprodseq  11510  gcdaddm  11902  bastop2  12625  restopn2  12724  iscnp3  12744  lmbr2  12755  txlm  12820  ismet2  12895  xblpnfps  12939  xblpnf  12940  blininf  12965  blres  12975  elmopn2  12990  neibl  13032  metrest  13047  metcnp3  13052  metcnp  13053  metcnp2  13054  metcn  13055  txmetcn  13060  cnbl0  13075  cnblcld  13076  bl2ioo  13083  elcncf2  13102  cncfmet  13120  cnlimc  13182