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  2492  reubida  2679  rmobida  2684  mpteq12f  4114  reuhypd  4507  funbrfv2b  5608  dffn5im  5609  eqfnfv2  5663  fndmin  5672  fniniseg  5685  rexsupp  5689  fmptco  5731  dff13  5818  riotabidva  5897  mpoeq123dva  5987  mpoeq3dva  5990  mpoxopovel  6308  qliftfun  6685  erovlem  6695  xpcomco  6894  pw2f1odclem  6904  elfi2  7047  ctssdccl  7186  ltexpi  7421  dfplpq2  7438  axprecex  7964  zrevaddcl  9393  qrevaddcl  9735  icoshft  10082  fznn  10181  shftdm  11004  2shfti  11013  sumeq2  11541  fsum3  11569  fsum2dlemstep  11616  prodeq2  11739  fprodseq  11765  bitsmod  12138  bitscmp  12140  gcdaddm  12176  grpidpropdg  13076  ismgmid  13079  gsumpropd2  13095  mhmpropd  13168  issubm2  13175  eqgid  13432  eqgabl  13536  rngpropd  13587  iscrng2  13647  ringpropd  13670  crngpropd  13671  crngunit  13743  dvdsrpropdg  13779  issubrg3  13879  lsslss  14013  lsspropdg  14063  znleval  14285  bastop2  14404  restopn2  14503  iscnp3  14523  lmbr2  14534  txlm  14599  ismet2  14674  xblpnfps  14718  xblpnf  14719  blininf  14744  blres  14754  elmopn2  14769  neibl  14811  metrest  14826  metcnp3  14831  metcnp  14832  metcnp2  14833  metcn  14834  txmetcn  14839  cnbl0  14854  cnblcld  14855  bl2ioo  14870  elcncf2  14894  cncfmet  14912  cnlimc  14992  lgsquadlem1  15402  lgsquadlem2  15403  2lgslem1a  15413