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 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜃)))

This proof depends on syntax axioms:   → wi 4   ∧ wa 104   ↔ wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  rexbida  2545  reubida  2734  rmobida  2740  mpteq12f  4212  reuhypd  4619  funbrfv2b  5750  dffn5im  5751  eqfnfv2  5810  fndmin  5819  fniniseg  5832  fmptco  5877  dff13  5977  riotabidva  6059  mpoeq123dva  6152  mpoeq3dva  6155  suppssrst  6505  suppssrgst  6506  suppinisegdc  6513  mpoxopovel  6517  qliftfun  6896  erovlem  6906  mapsnend  7105  xpcomco  7130  pw2f1odclem  7140  elfi2  7312  ctssdccl  7458  ltexpi  7711  dfplpq2  7728  axprecex  8254  zrevaddcl  9705  qrevaddcl  10060  icoshft  10409  fznn  10513  sseqn  11301  pfxeq  11490  pfxsuffeqwrdeq  11492  pfxsuff1eqwrdeq  11493  shftdm  11609  2shfti  11618  sumeq2  12150  fsum3  12179  fsum2dlemstep  12226  prodeq2  12349  fprodseq  12375  bitsmod  12748  bitscmp  12750  gcdaddm  12786  grpidpropdg  13753  ismgmid  13756  mhmpropd  13832  issubm2  13839  eqgid  14088  eqgabl  14224  rngpropd  14361  iscrng2  14426  ringpropd  14450  crngpropd  14451  crngunit  14527  dvdsrpropdg  14563  issubrg3  14664  lsslss  14827  lsspropdg  14877  znleval  15097  bastop2  15343  restopn2  15442  iscnp3  15462  lmbr2  15473  txlm  15538  ismet2  15613  xblpnfps  15657  xblpnf  15658  blininf  15683  blres  15693  elmopn2  15708  neibl  15750  metrest  15765  metcnp3  15770  metcnp  15771  metcnp2  15772  metcn  15773  txmetcn  15778  cnbl0  15793  cnblcld  15794  bl2ioo  15809  elcncf2  15833  cncfmet  15851  cnlimc  15931  lgsquadlem1  16434  lgsquadlem2  16435  2lgslem1a  16445  upgriswlkdc  16839  isclwwlknx  16895  clwwlkn1  16897  clwwlkn2  16900  eupth2lemsfi  16957