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  2527  reubida  2715  rmobida  2721  mpteq12f  4169  reuhypd  4568  funbrfv2b  5690  dffn5im  5691  eqfnfv2  5745  fndmin  5754  fniniseg  5767  rexsupp  5771  fmptco  5813  dff13  5909  riotabidva  5989  mpoeq123dva  6082  mpoeq3dva  6085  mpoxopovel  6407  qliftfun  6786  erovlem  6796  xpcomco  7010  pw2f1odclem  7020  elfi2  7171  ctssdccl  7310  ltexpi  7557  dfplpq2  7574  axprecex  8100  zrevaddcl  9530  qrevaddcl  9878  icoshft  10225  fznn  10324  pfxeq  11281  pfxsuffeqwrdeq  11283  pfxsuff1eqwrdeq  11284  shftdm  11387  2shfti  11396  sumeq2  11924  fsum3  11953  fsum2dlemstep  12000  prodeq2  12123  fprodseq  12149  bitsmod  12522  bitscmp  12524  gcdaddm  12560  grpidpropdg  13462  ismgmid  13465  gsumpropd2  13481  mhmpropd  13554  issubm2  13561  eqgid  13818  eqgabl  13922  rngpropd  13974  iscrng2  14034  ringpropd  14057  crngpropd  14058  crngunit  14131  dvdsrpropdg  14167  issubrg3  14267  lsslss  14401  lsspropdg  14451  znleval  14673  bastop2  14814  restopn2  14913  iscnp3  14933  lmbr2  14944  txlm  15009  ismet2  15084  xblpnfps  15128  xblpnf  15129  blininf  15154  blres  15164  elmopn2  15179  neibl  15221  metrest  15236  metcnp3  15241  metcnp  15242  metcnp2  15243  metcn  15244  txmetcn  15249  cnbl0  15264  cnblcld  15265  bl2ioo  15280  elcncf2  15304  cncfmet  15322  cnlimc  15402  lgsquadlem1  15812  lgsquadlem2  15813  2lgslem1a  15823  upgriswlkdc  16217  isclwwlknx  16273  clwwlkn1  16275  clwwlkn2  16278  eupth2lemsfi  16335