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  6916  mapxpen  6918  en2eleq  7276  nnledivrp  9860  xsubge0  9975  iccen  10100  fldiv4lem1div2uz2  10415  frec2uzsucd  10512  seqp1g  10577  seq3shft  11022  geolim2  11696  geoisum1c  11704  ntrivcvgap  11732  eflegeo  11885  sin01gt0  11946  cos01gt0  11947  3dvds  12048  gcdn0gt0  12172  uzwodc  12231  divgcdodd  12338  sqpweven  12370  2sqpwodd  12371  pythagtriplem4  12464  pythagtriplem11  12470  pythagtriplem12  12471  pythagtriplem13  12472  pythagtriplem14  12473  pcfac  12546  4sqlemffi  12592  omctfn  12687  ssnnctlemct  12690  topnvalg  12955  imasmulr  13013  imasaddfnlemg  13018  gsumsplit1r  13102  gsumprval  13103  ismhm  13165  mhmex  13166  gsumfzz  13199  prdsinvlem  13312  scaffng  13943  lss1d  14017  zringinvg  14238  psrplusgg  14312  restbasg  14512  restco  14518  lmfval  14536  cnfval  14538  cnpval  14542  upxp  14616  uptx  14618  txrest  14620  xblm  14761  bdmet  14846  bdmopn  14848  reopnap  14890  cnopnap  14955  maxcncf  14959  mincncf  14960  dvidlemap  15035  dvcj  15053  plyval  15076  plysub  15097  eflt  15119  logdivlti  15225  perfectlem1  15343  perfectlem2  15344  gausslemma2dlem0i  15406  gausslemma2dlem4  15413  lgsquad2lem1  15430  lgsquad2lem2  15431  trilpolemisumle  15795