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  2525  reubida  2713  rmobida  2719  mpteq12f  4163  reuhypd  4559  funbrfv2b  5671  dffn5im  5672  eqfnfv2  5726  fndmin  5735  fniniseg  5748  rexsupp  5752  fmptco  5794  dff13  5885  riotabidva  5965  mpoeq123dva  6056  mpoeq3dva  6059  mpoxopovel  6377  qliftfun  6754  erovlem  6764  xpcomco  6973  pw2f1odclem  6983  elfi2  7127  ctssdccl  7266  ltexpi  7512  dfplpq2  7529  axprecex  8055  zrevaddcl  9485  qrevaddcl  9827  icoshft  10174  fznn  10273  pfxeq  11214  pfxsuffeqwrdeq  11216  pfxsuff1eqwrdeq  11217  shftdm  11319  2shfti  11328  sumeq2  11856  fsum3  11884  fsum2dlemstep  11931  prodeq2  12054  fprodseq  12080  bitsmod  12453  bitscmp  12455  gcdaddm  12491  grpidpropdg  13393  ismgmid  13396  gsumpropd2  13412  mhmpropd  13485  issubm2  13492  eqgid  13749  eqgabl  13853  rngpropd  13904  iscrng2  13964  ringpropd  13987  crngpropd  13988  crngunit  14060  dvdsrpropdg  14096  issubrg3  14196  lsslss  14330  lsspropdg  14380  znleval  14602  bastop2  14743  restopn2  14842  iscnp3  14862  lmbr2  14873  txlm  14938  ismet2  15013  xblpnfps  15057  xblpnf  15058  blininf  15083  blres  15093  elmopn2  15108  neibl  15150  metrest  15165  metcnp3  15170  metcnp  15171  metcnp2  15172  metcn  15173  txmetcn  15178  cnbl0  15193  cnblcld  15194  bl2ioo  15209  elcncf2  15233  cncfmet  15251  cnlimc  15331  lgsquadlem1  15741  lgsquadlem2  15742  2lgslem1a  15752