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  2528  reubida  2716  rmobida  2722  mpteq12f  4174  reuhypd  4574  funbrfv2b  5699  dffn5im  5700  eqfnfv2  5754  fndmin  5763  fniniseg  5776  fmptco  5821  dff13  5919  riotabidva  5999  mpoeq123dva  6092  mpoeq3dva  6095  suppssrst  6439  suppssrgst  6440  mpoxopovel  6450  qliftfun  6829  erovlem  6839  xpcomco  7053  pw2f1odclem  7063  elfi2  7214  ctssdccl  7353  ltexpi  7600  dfplpq2  7617  axprecex  8143  zrevaddcl  9573  qrevaddcl  9921  icoshft  10268  fznn  10367  pfxeq  11324  pfxsuffeqwrdeq  11326  pfxsuff1eqwrdeq  11327  shftdm  11443  2shfti  11452  sumeq2  11980  fsum3  12009  fsum2dlemstep  12056  prodeq2  12179  fprodseq  12205  bitsmod  12578  bitscmp  12580  gcdaddm  12616  grpidpropdg  13518  ismgmid  13521  gsumpropd2  13537  mhmpropd  13610  issubm2  13617  eqgid  13874  eqgabl  13978  rngpropd  14030  iscrng2  14090  ringpropd  14113  crngpropd  14114  crngunit  14187  dvdsrpropdg  14223  issubrg3  14323  lsslss  14457  lsspropdg  14507  znleval  14729  bastop2  14875  restopn2  14974  iscnp3  14994  lmbr2  15005  txlm  15070  ismet2  15145  xblpnfps  15189  xblpnf  15190  blininf  15215  blres  15225  elmopn2  15240  neibl  15282  metrest  15297  metcnp3  15302  metcnp  15303  metcnp2  15304  metcn  15305  txmetcn  15310  cnbl0  15325  cnblcld  15326  bl2ioo  15341  elcncf2  15365  cncfmet  15383  cnlimc  15463  lgsquadlem1  15876  lgsquadlem2  15877  2lgslem1a  15887  upgriswlkdc  16281  isclwwlknx  16337  clwwlkn1  16339  clwwlkn2  16342  eupth2lemsfi  16399