Theorem pm5.32da 456

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 454	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  2545  reubida  2734  rmobida  2740  mpteq12f  4209  reuhypd  4615  funbrfv2b  5744  dffn5im  5745  eqfnfv2  5801  fndmin  5810  fniniseg  5823  fmptco  5868  dff13  5968  riotabidva  6050  mpoeq123dva  6143  mpoeq3dva  6146  suppssrst  6495  suppssrgst  6496  mpoxopovel  6506  qliftfun  6885  erovlem  6895  mapsnend  7093  xpcomco  7118  pw2f1odclem  7128  elfi2  7300  ctssdccl  7445  ltexpi  7698  dfplpq2  7715  axprecex  8241  zrevaddcl  9678  qrevaddcl  10027  icoshft  10375  fznn  10479  sseqn  11262  pfxeq  11451  pfxsuffeqwrdeq  11453  pfxsuff1eqwrdeq  11454  shftdm  11570  2shfti  11579  sumeq2  12108  fsum3  12137  fsum2dlemstep  12184  prodeq2  12307  fprodseq  12333  bitsmod  12706  bitscmp  12708  gcdaddm  12744  grpidpropdg  13677  ismgmid  13680  mhmpropd  13756  issubm2  13763  eqgid  14012  eqgabl  14117  rngpropd  14237  iscrng2  14302  ringpropd  14326  crngpropd  14327  crngunit  14401  dvdsrpropdg  14437  issubrg3  14538  lsslss  14701  lsspropdg  14751  znleval  14971  bastop2  15168  restopn2  15267  iscnp3  15287  lmbr2  15298  txlm  15363  ismet2  15438  xblpnfps  15482  xblpnf  15483  blininf  15508  blres  15518  elmopn2  15533  neibl  15575  metrest  15590  metcnp3  15595  metcnp  15596  metcnp2  15597  metcn  15598  txmetcn  15603  cnbl0  15618  cnblcld  15619  bl2ioo  15634  elcncf2  15658  cncfmet  15676  cnlimc  15756  lgsquadlem1  16179  lgsquadlem2  16180  2lgslem1a  16190  upgriswlkdc  16584  isclwwlknx  16640  clwwlkn1  16642  clwwlkn2  16645  eupth2lemsfi  16702