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  6907  mapxpen  6909  en2eleq  7262  nnledivrp  9841  xsubge0  9956  iccen  10081  fldiv4lem1div2uz2  10396  frec2uzsucd  10493  seqp1g  10558  seq3shft  11003  geolim2  11677  geoisum1c  11685  ntrivcvgap  11713  eflegeo  11866  sin01gt0  11927  cos01gt0  11928  3dvds  12029  gcdn0gt0  12145  uzwodc  12204  divgcdodd  12311  sqpweven  12343  2sqpwodd  12344  pythagtriplem4  12437  pythagtriplem11  12443  pythagtriplem12  12444  pythagtriplem13  12445  pythagtriplem14  12446  pcfac  12519  4sqlemffi  12565  omctfn  12660  ssnnctlemct  12663  topnvalg  12922  imasmulr  12952  imasaddfnlemg  12957  gsumsplit1r  13041  gsumprval  13042  ismhm  13093  mhmex  13094  gsumfzz  13127  scaffng  13865  lss1d  13939  zringinvg  14160  psrplusgg  14230  restbasg  14404  restco  14410  lmfval  14428  cnfval  14430  cnpval  14434  upxp  14508  uptx  14510  txrest  14512  xblm  14653  bdmet  14738  bdmopn  14740  reopnap  14782  cnopnap  14847  maxcncf  14851  mincncf  14852  dvidlemap  14927  dvcj  14945  plyval  14968  plysub  14989  eflt  15011  logdivlti  15117  perfectlem1  15235  perfectlem2  15236  gausslemma2dlem0i  15298  gausslemma2dlem4  15305  lgsquad2lem1  15322  lgsquad2lem2  15323  trilpolemisumle  15682