Theorem syl2and 609

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 606	. 2 ⊢ (𝜑 → ((𝜒 ∧ 𝜃) → 𝜂))
5	1, 4	syland 604	1 ⊢ (𝜑 → ((𝜓 ∧ 𝜃) → 𝜂))

Syntax hints:   → wi 4   ∧ wa 397

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 206  df-an 398

This theorem is referenced by:  anim12d  610  ax7  2020  dffi3  9426  cflim2  10258  axpre-sup  11164  xle2add  13238  fzen  13518  rpmulgcd2  16593  pcqmul  16786  sbcie2s  17094  initoeu1  17961  termoeu1  17968  plttr  18295  pospo  18298  lublecllem  18313  latjlej12  18408  latmlem12  18424  hausnei2  22857  uncmp  22907  itgsubst  25566  dvdsmulf1o  26698  2sqlem8a  26928  precsexlem10  27662  axcontlem9  28230  uspgr2wlkeq  28903  shintcli  30582  cvntr  31545  cdj3i  31694  f1resrcmplf1dlem  34089  satffunlem  34392  bj-bary1  36193  heicant  36523  itg2addnc  36542  dihmeetlem1N  40161  fmtnofac2lem  46236  2itscp  47467  mofsn  47510