Theorem pm5.32da 452

Description: Distribution of implication over biconditional (deduction form). (Contributed by NM, 9-Dec-2006.)

Hypothesis

Ref	Expression
pm5.32da.1	⊢ ((𝜑 ∧ 𝜓) → (𝜒 ↔ 𝜃))

Assertion

Ref	Expression
pm5.32da	⊢ (𝜑 → ((𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜃)))

Proof of Theorem pm5.32da

Step	Hyp	Ref	Expression
1		pm5.32da.1	. . 3 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 ↔ 𝜃))
2	1	ex 115	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 ↔ 𝜃)))
3	2	pm5.32d 450	1 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜃)))

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  2525  reubida  2713  rmobida  2719  mpteq12f  4164  reuhypd  4562  funbrfv2b  5680  dffn5im  5681  eqfnfv2  5735  fndmin  5744  fniniseg  5757  rexsupp  5761  fmptco  5803  dff13  5898  riotabidva  5978  mpoeq123dva  6071  mpoeq3dva  6074  mpoxopovel  6393  qliftfun  6772  erovlem  6782  xpcomco  6993  pw2f1odclem  7003  elfi2  7147  ctssdccl  7286  ltexpi  7532  dfplpq2  7549  axprecex  8075  zrevaddcl  9505  qrevaddcl  9847  icoshft  10194  fznn  10293  pfxeq  11236  pfxsuffeqwrdeq  11238  pfxsuff1eqwrdeq  11239  shftdm  11341  2shfti  11350  sumeq2  11878  fsum3  11906  fsum2dlemstep  11953  prodeq2  12076  fprodseq  12102  bitsmod  12475  bitscmp  12477  gcdaddm  12513  grpidpropdg  13415  ismgmid  13418  gsumpropd2  13434  mhmpropd  13507  issubm2  13514  eqgid  13771  eqgabl  13875  rngpropd  13926  iscrng2  13986  ringpropd  14009  crngpropd  14010  crngunit  14083  dvdsrpropdg  14119  issubrg3  14219  lsslss  14353  lsspropdg  14403  znleval  14625  bastop2  14766  restopn2  14865  iscnp3  14885  lmbr2  14896  txlm  14961  ismet2  15036  xblpnfps  15080  xblpnf  15081  blininf  15106  blres  15116  elmopn2  15131  neibl  15173  metrest  15188  metcnp3  15193  metcnp  15194  metcnp2  15195  metcn  15196  txmetcn  15201  cnbl0  15216  cnblcld  15217  bl2ioo  15232  elcncf2  15256  cncfmet  15274  cnlimc  15354  lgsquadlem1  15764  lgsquadlem2  15765  2lgslem1a  15775  upgriswlkdc  16081