Theorem mp3an2i 1355

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

Syntax hints:   → wi 4   ∧ w3a 981

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 983

This theorem is referenced by:  mapen  6963  mapxpen  6965  en2eleq  7329  nnledivrp  9918  xsubge0  10033  iccen  10158  fldiv4lem1div2uz2  10481  frec2uzsucd  10578  seqp1g  10643  fnpfx  11163  seq3shft  11234  geolim2  11908  geoisum1c  11916  ntrivcvgap  11944  eflegeo  12097  sin01gt0  12158  cos01gt0  12159  3dvds  12260  gcdn0gt0  12384  uzwodc  12443  divgcdodd  12550  sqpweven  12582  2sqpwodd  12583  pythagtriplem4  12676  pythagtriplem11  12682  pythagtriplem12  12683  pythagtriplem13  12684  pythagtriplem14  12685  pcfac  12758  4sqlemffi  12804  omctfn  12899  ssnnctlemct  12902  topnvalg  13168  imasmulr  13226  imasaddfnlemg  13231  gsumsplit1r  13315  gsumprval  13316  ismhm  13378  mhmex  13379  gsumfzz  13412  prdsinvlem  13525  scaffng  14156  lss1d  14230  zringinvg  14451  psrplusgg  14525  restbasg  14725  restco  14731  lmfval  14749  cnfval  14751  cnpval  14755  upxp  14829  uptx  14831  txrest  14833  xblm  14974  bdmet  15059  bdmopn  15061  reopnap  15103  cnopnap  15168  maxcncf  15172  mincncf  15173  dvidlemap  15248  dvcj  15266  plyval  15289  plysub  15310  eflt  15332  logdivlti  15438  perfectlem1  15556  perfectlem2  15557  gausslemma2dlem0i  15619  gausslemma2dlem4  15626  lgsquad2lem1  15643  lgsquad2lem2  15644  trilpolemisumle  16149