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  2472  reubida  2658  rmobida  2663  mpteq12f  4083  reuhypd  4471  funbrfv2b  5560  dffn5im  5561  eqfnfv2  5614  fndmin  5623  fniniseg  5636  rexsupp  5640  fmptco  5682  dff13  5768  riotabidva  5846  mpoeq123dva  5935  mpoeq3dva  5938  mpoxopovel  6241  qliftfun  6616  erovlem  6626  xpcomco  6825  elfi2  6970  ctssdccl  7109  ltexpi  7335  dfplpq2  7352  axprecex  7878  zrevaddcl  9301  qrevaddcl  9642  icoshft  9988  fznn  10086  shftdm  10826  2shfti  10835  sumeq2  11362  fsum3  11390  fsum2dlemstep  11437  prodeq2  11560  fprodseq  11586  gcdaddm  11979  grpidpropdg  12747  ismgmid  12750  mhmpropd  12811  issubm2  12818  eqgid  13038  iscrng2  13151  ringpropd  13170  crngpropd  13171  crngunit  13233  dvdsrpropdg  13269  issubrg3  13328  bastop2  13477  restopn2  13576  iscnp3  13596  lmbr2  13607  txlm  13672  ismet2  13747  xblpnfps  13791  xblpnf  13792  blininf  13817  blres  13827  elmopn2  13842  neibl  13884  metrest  13899  metcnp3  13904  metcnp  13905  metcnp2  13906  metcn  13907  txmetcn  13912  cnbl0  13927  cnblcld  13928  bl2ioo  13935  elcncf2  13954  cncfmet  13972  cnlimc  14034