Theorem syl2and 608

Description: A syllogism deduction. (Contributed by NM, 15-Dec-2004.)

Hypotheses

Ref	Expression
syl2and.1	⊢ (𝜑 → (𝜓 → 𝜒))
syl2and.2	⊢ (𝜑 → (𝜃 → 𝜏))
syl2and.3	⊢ (𝜑 → ((𝜒 ∧ 𝜏) → 𝜂))

Assertion

Ref	Expression
syl2and	⊢ (𝜑 → ((𝜓 ∧ 𝜃) → 𝜂))

Proof of Theorem syl2and

Step	Hyp	Ref	Expression
1		syl2and.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
2		syl2and.2	. . 3 ⊢ (𝜑 → (𝜃 → 𝜏))
3		syl2and.3	. . 3 ⊢ (𝜑 → ((𝜒 ∧ 𝜏) → 𝜂))
4	2, 3	sylan2d 605	. 2 ⊢ (𝜑 → ((𝜒 ∧ 𝜃) → 𝜂))
5	1, 4	syland 603	1 ⊢ (𝜑 → ((𝜓 ∧ 𝜃) → 𝜂))

Syntax hints:   → wi 4   ∧ wa 395

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 207  df-an 396

This theorem is referenced by:  anim12d  609  ax7  2016  dffi3  9389  cflim2  10223  axpre-sup  11129  xle2add  13226  fzen  13509  rpmulgcd2  16633  pcqmul  16831  sbcie2s  17138  initoeu1  17980  termoeu1  17987  plttr  18308  pospo  18311  lublecllem  18326  latjlej12  18421  latmlem12  18437  hausnei2  23247  uncmp  23297  itgsubst  25963  mpodvdsmulf1o  27111  dvdsmulf1o  27113  2sqlem8a  27343  precsexlem10  28125  axcontlem9  28906  uspgr2wlkeq  29581  shintcli  31265  cvntr  32228  cdj3i  32377  f1resrcmplf1dlem  35083  satffunlem  35395  bj-bary1  37307  heicant  37656  itg2addnc  37675  dihmeetlem1N  41291  modelaxreplem1  44975  fmtnofac2lem  47573  2itscp  48774  mofsn  48836