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  2539  reubida  2728  rmobida  2734  mpteq12f  4195  reuhypd  4597  funbrfv2b  5726  dffn5im  5727  eqfnfv2  5781  fndmin  5790  fniniseg  5803  fmptco  5848  dff13  5947  riotabidva  6029  mpoeq123dva  6122  mpoeq3dva  6125  suppssrst  6474  suppssrgst  6475  mpoxopovel  6485  qliftfun  6864  erovlem  6874  mapsnend  7065  xpcomco  7090  pw2f1odclem  7100  elfi2  7272  ctssdccl  7415  ltexpi  7668  dfplpq2  7685  axprecex  8211  zrevaddcl  9648  qrevaddcl  9997  icoshft  10345  fznn  10448  sseqn  11231  pfxeq  11416  pfxsuffeqwrdeq  11418  pfxsuff1eqwrdeq  11419  shftdm  11535  2shfti  11544  sumeq2  12073  fsum3  12102  fsum2dlemstep  12149  prodeq2  12272  fprodseq  12298  bitsmod  12671  bitscmp  12673  gcdaddm  12709  grpidpropdg  13641  ismgmid  13644  gsumpropd2  13660  mhmpropd  13725  issubm2  13732  eqgid  13983  eqgabl  14087  rngpropd  14198  iscrng2  14262  ringpropd  14285  crngpropd  14286  crngunit  14360  dvdsrpropdg  14396  issubrg3  14497  lsslss  14659  lsspropdg  14709  znleval  14931  bastop2  15079  restopn2  15178  iscnp3  15198  lmbr2  15209  txlm  15274  ismet2  15349  xblpnfps  15393  xblpnf  15394  blininf  15419  blres  15429  elmopn2  15444  neibl  15486  metrest  15501  metcnp3  15506  metcnp  15507  metcnp2  15508  metcn  15509  txmetcn  15514  cnbl0  15529  cnblcld  15530  bl2ioo  15545  elcncf2  15569  cncfmet  15587  cnlimc  15667  lgsquadlem1  16080  lgsquadlem2  16081  2lgslem1a  16091  upgriswlkdc  16485  isclwwlknx  16541  clwwlkn1  16543  clwwlkn2  16546  eupth2lemsfi  16603