Theorem mp3an3an 1491

Description: mp3an 1485 with antecedents in standard conjunction form and with two hypotheses which are implications. (Contributed by Alan Sare, 28-Aug-2016.)

Hypotheses

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

Assertion

Ref	Expression
mp3an3an	⊢ ((𝜓 ∧ 𝜃) → 𝜂)

Proof of Theorem mp3an3an

Step	Hyp	Ref	Expression
1		mp3an3an.2	. 2 ⊢ (𝜓 → 𝜒)
2		mp3an3an.3	. 2 ⊢ (𝜃 → 𝜏)
3		mp3an3an.1	. . 3 ⊢ 𝜑
4		mp3an3an.4	. . 3 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) → 𝜂)
5	3, 4	mp3an1 1472	. 2 ⊢ ((𝜒 ∧ 𝜏) → 𝜂)
6	1, 2, 5	syl2an 607	1 ⊢ ((𝜓 ∧ 𝜃) → 𝜂)

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1101

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 210  df-an 401  df-3an 1103

This theorem is referenced by:  mp3an2ani  1492  unfilem2  9254  rankelun  9832  mul02  11376  fnn0ind  12683  supminf  12947  nn0p1elfzo  13719  faclbnd5  14322  pfxccatin12lem3  14757  mulre  15160  divalglem0  16439  algcvga  16625  infpn2  16961  prmgaplem7  17105  blssioo  24909  i1fsub  25824  itg1sub  25825  coesub  26371  dgrsub  26386  sincosq1eq  26631  logtayl2  26781  cxploglim  27096  uspgr2v1e2w  29506  ftc1anclem6  38204  fourierdlem48  46727  plusmod5ne  47944  muldvdsfacgt  47979  io1ii  49551