Theorem pm5.32da 445

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 443	1 |- ( ph -> ( ( ps /\ ch ) <-> ( ps /\ th ) ) )

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

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  rexbida  2406  reubida  2586  rmobida  2591  mpteq12f  3968  reuhypd  4352  funbrfv2b  5420  dffn5im  5421  eqfnfv2  5473  fndmin  5481  fniniseg  5494  rexsupp  5498  fmptco  5540  dff13  5623  riotabidva  5700  mpoeq123dva  5786  mpoeq3dva  5789  mpoxopovel  6092  qliftfun  6465  erovlem  6475  xpcomco  6673  elfi2  6812  ctssdccl  6948  ltexpi  7090  dfplpq2  7107  axprecex  7612  zrevaddcl  9005  qrevaddcl  9335  icoshft  9663  fznn  9759  shftdm  10484  2shfti  10493  sumeq2  11017  fsum3  11045  fsum2dlemstep  11092  gcdaddm  11517  bastop2  12093  restopn2  12192  iscnp3  12211  lmbr2  12222  txlm  12287  ismet2  12340  xblpnfps  12384  xblpnf  12385  blininf  12410  blres  12420  elmopn2  12435  neibl  12477  metrest  12492  metcnp3  12497  metcnp  12498  metcnp2  12499  metcn  12500  txmetcn  12505  cnbl0  12520  cnblcld  12521  bl2ioo  12525  elcncf2  12544  cncfmet  12562  cnlimc  12594