Theorem mp3an2i 1353

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

Syntax hints:   → wi 4   ∧ w3a 980

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117  df-3an 982

This theorem is referenced by:  mapen  6874  mapxpen  6876  en2eleq  7224  nnledivrp  9796  xsubge0  9911  iccen  10036  frec2uzsucd  10432  seq3shft  10879  geolim2  11552  geoisum1c  11560  ntrivcvgap  11588  eflegeo  11741  sin01gt0  11801  cos01gt0  11802  gcdn0gt0  12011  uzwodc  12070  divgcdodd  12175  sqpweven  12207  2sqpwodd  12208  pythagtriplem4  12300  pythagtriplem11  12306  pythagtriplem12  12307  pythagtriplem13  12308  pythagtriplem14  12309  pcfac  12382  4sqlemffi  12428  omctfn  12494  ssnnctlemct  12497  topnvalg  12756  imasmulr  12786  imasaddfnlemg  12791  ismhm  12913  mhmex  12914  scaffng  13625  lss1d  13699  zringinvg  13903  restbasg  14125  restco  14131  lmfval  14149  cnfval  14151  cnpval  14155  upxp  14229  uptx  14231  txrest  14233  xblm  14374  bdmet  14459  bdmopn  14461  reopnap  14495  cnopnap  14551  dvidlemap  14617  dvcj  14630  eflt  14653  logdivlti  14759  trilpolemisumle  15245