Theorem mp3an2i 1421

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

Syntax hints:   → wi 4   ∧ w3a 1031

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 196  df-an 385  df-3an 1033

This theorem is referenced by:  nnledivrp  11816  wrdlen2i  13534  0.999...  14451  fsumcube  14630  3dvds  14890  cnaddinv  18097  opsrtoslem2  19306  frgpcyg  19741  pt1hmeo  21419  cnheiborlem  22561  lgsqrlem4  24874  gausslemma2dlem4  24894  lgsquad2lem2  24910  enrelmap  37311  k0004lem3  37467  sineq0ALT  38195  odz2prm2pw  40013  fmtno4prmfac  40022  lighneallem3  40062  lighneallem4a  40063  lighneallem4  40065  1wlkp1lem3  40884  1wlkp1lem7  40888  1wlkp1lem8  40889  pthdlem1  40972  conngrv2edg  41362