Theorem mp3an2i 1591

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

Hypotheses

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

Assertion

Ref	Expression
mp3an2i	⊢ (𝜓 → 𝜏)

Proof of Theorem mp3an2i

Step	Hyp	Ref	Expression
1		mp3an2i.2	. 2 ⊢ (𝜓 → 𝜒)
2		mp3an2i.3	. 2 ⊢ (𝜓 → 𝜃)
3		mp3an2i.1	. . 3 ⊢ 𝜑
4		mp3an2i.4	. . 3 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → 𝜏)
5	3, 4	mp3an1 1573	. 2 ⊢ ((𝜒 ∧ 𝜃) → 𝜏)
6	1, 2, 5	syl2anc 580	1 ⊢ (𝜓 → 𝜏)

Syntax hints:   → wi 4   ∧ w3a 1108

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 199  df-an 386  df-3an 1110

This theorem is referenced by:  nnledivrp  12183  wrdlen2i  14024  sqrlem7  14327  0.999...  14947  fsumcube  15124  sin01gt0  15253  cos01gt0  15254  3dvds  15388  nno  15431  divgcdodd  15752  cnaddinv  18586  opsrtoslem2  19804  frgpcyg  20240  pt1hmeo  21935  metustid  22684  cnheiborlem  23078  lgsqrlem4  25423  gausslemma2dlem4  25443  lgsquad2lem2  25459  wlkp1lem3  26920  wlkp1lem7  26924  wlkp1lem8  26925  pthdlem1  27012  conngrv2edg  27531  cvmlift2lem10  31803  frrlem11  32297  nosupbday  32356  itg2gt0cn  33945  enrelmap  39061  k0004lem3  39217  sineq0ALT  39921  xlimconst  40783  odz2prm2pw  42245  fmtno4prmfac  42254  lighneallem3  42294  lighneallem4a  42295  lighneallem4  42297