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  2659  rmobida  2664  mpteq12f  4084  reuhypd  4472  funbrfv2b  5561  dffn5im  5562  eqfnfv2  5615  fndmin  5624  fniniseg  5637  rexsupp  5641  fmptco  5683  dff13  5769  riotabidva  5847  mpoeq123dva  5936  mpoeq3dva  5939  mpoxopovel  6242  qliftfun  6617  erovlem  6627  xpcomco  6826  elfi2  6971  ctssdccl  7110  ltexpi  7336  dfplpq2  7353  axprecex  7879  zrevaddcl  9303  qrevaddcl  9644  icoshft  9990  fznn  10089  shftdm  10831  2shfti  10840  sumeq2  11367  fsum3  11395  fsum2dlemstep  11442  prodeq2  11565  fprodseq  11591  gcdaddm  11985  grpidpropdg  12793  ismgmid  12796  mhmpropd  12857  issubm2  12864  eqgid  13085  iscrng2  13198  ringpropd  13217  crngpropd  13218  crngunit  13280  dvdsrpropdg  13316  issubrg3  13368  bastop2  13587  restopn2  13686  iscnp3  13706  lmbr2  13717  txlm  13782  ismet2  13857  xblpnfps  13901  xblpnf  13902  blininf  13927  blres  13937  elmopn2  13952  neibl  13994  metrest  14009  metcnp3  14014  metcnp  14015  metcnp2  14016  metcn  14017  txmetcn  14022  cnbl0  14037  cnblcld  14038  bl2ioo  14045  elcncf2  14064  cncfmet  14082  cnlimc  14144