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  2502  reubida  2689  rmobida  2694  mpteq12f  4129  reuhypd  4523  funbrfv2b  5633  dffn5im  5634  eqfnfv2  5688  fndmin  5697  fniniseg  5710  rexsupp  5714  fmptco  5756  dff13  5847  riotabidva  5926  mpoeq123dva  6016  mpoeq3dva  6019  mpoxopovel  6337  qliftfun  6714  erovlem  6724  xpcomco  6933  pw2f1odclem  6943  elfi2  7086  ctssdccl  7225  ltexpi  7463  dfplpq2  7480  axprecex  8006  zrevaddcl  9436  qrevaddcl  9778  icoshft  10125  fznn  10224  pfxeq  11161  pfxsuffeqwrdeq  11163  pfxsuff1eqwrdeq  11164  shftdm  11183  2shfti  11192  sumeq2  11720  fsum3  11748  fsum2dlemstep  11795  prodeq2  11918  fprodseq  11944  bitsmod  12317  bitscmp  12319  gcdaddm  12355  grpidpropdg  13256  ismgmid  13259  gsumpropd2  13275  mhmpropd  13348  issubm2  13355  eqgid  13612  eqgabl  13716  rngpropd  13767  iscrng2  13827  ringpropd  13850  crngpropd  13851  crngunit  13923  dvdsrpropdg  13959  issubrg3  14059  lsslss  14193  lsspropdg  14243  znleval  14465  bastop2  14606  restopn2  14705  iscnp3  14725  lmbr2  14736  txlm  14801  ismet2  14876  xblpnfps  14920  xblpnf  14921  blininf  14946  blres  14956  elmopn2  14971  neibl  15013  metrest  15028  metcnp3  15033  metcnp  15034  metcnp2  15035  metcn  15036  txmetcn  15041  cnbl0  15056  cnblcld  15057  bl2ioo  15072  elcncf2  15096  cncfmet  15114  cnlimc  15194  lgsquadlem1  15604  lgsquadlem2  15605  2lgslem1a  15615