Theorem mp3an3an 1496

Description: mp3an 1490 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 1477	. 2 ⊢ ((𝜒 ∧ 𝜏) → 𝜂)
6	1, 2, 5	syl2an 608	1 ⊢ ((𝜓 ∧ 𝜃) → 𝜂)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  mp3an2ani  1497  unfilem2  9298  rankelun  9889  mul02  11488  fnn0ind  12798  supminf  13062  nn0p1elfzo  13837  faclbnd5  14442  pfxccatin12lem3  14881  mulre  15288  divalglem0  16563  algcvga  16754  infpn2  17091  prmgaplem7  17235  blssioo  25114  i1fsub  26029  itg1sub  26030  coesub  26576  dgrsub  26591  sincosq1eq  26841  logtayl2  26990  cxploglim  27305  uspgr2v1e2w  29832  ftc1anclem6  38617  findcard4  38633  fourierdlem48  47164  plusmod5ne  48421  muldvdsfacgt  48456  io1ii  50029