Theorem mp3an2i 1429

Description: mp3an 1424 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 1411	. 2 ⊢ ((𝜒 ∧ 𝜃) → 𝜏)
6	1, 2, 5	syl2anc 693	1 ⊢ (𝜓 → 𝜏)

Syntax hints:   → wi 4   ∧ w3a 1037

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 197  df-an 386  df-3an 1039

This theorem is referenced by:  nnledivrp  11940  wrdlen2i  13686  0.999...  14612  fsumcube  14791  3dvds  15052  divgcdodd  15422  cnaddinv  18274  opsrtoslem2  19485  frgpcyg  19922  pt1hmeo  21609  cnheiborlem  22753  lgsqrlem4  25074  gausslemma2dlem4  25094  lgsquad2lem2  25110  wlkp1lem3  26572  wlkp1lem7  26576  wlkp1lem8  26577  pthdlem1  26662  conngrv2edg  27055  cvmlift2lem10  31294  nosupbday  31851  enrelmap  38291  k0004lem3  38447  sineq0ALT  39173  xlimconst  40051  odz2prm2pw  41475  fmtno4prmfac  41484  lighneallem3  41524  lighneallem4a  41525  lighneallem4  41527