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  6945  mapxpen  6947  en2eleq  7305  nnledivrp  9890  xsubge0  10005  iccen  10130  fldiv4lem1div2uz2  10451  frec2uzsucd  10548  seqp1g  10613  seq3shft  11182  geolim2  11856  geoisum1c  11864  ntrivcvgap  11892  eflegeo  12045  sin01gt0  12106  cos01gt0  12107  3dvds  12208  gcdn0gt0  12332  uzwodc  12391  divgcdodd  12498  sqpweven  12530  2sqpwodd  12531  pythagtriplem4  12624  pythagtriplem11  12630  pythagtriplem12  12631  pythagtriplem13  12632  pythagtriplem14  12633  pcfac  12706  4sqlemffi  12752  omctfn  12847  ssnnctlemct  12850  topnvalg  13116  imasmulr  13174  imasaddfnlemg  13179  gsumsplit1r  13263  gsumprval  13264  ismhm  13326  mhmex  13327  gsumfzz  13360  prdsinvlem  13473  scaffng  14104  lss1d  14178  zringinvg  14399  psrplusgg  14473  restbasg  14673  restco  14679  lmfval  14697  cnfval  14699  cnpval  14703  upxp  14777  uptx  14779  txrest  14781  xblm  14922  bdmet  15007  bdmopn  15009  reopnap  15051  cnopnap  15116  maxcncf  15120  mincncf  15121  dvidlemap  15196  dvcj  15214  plyval  15237  plysub  15258  eflt  15280  logdivlti  15386  perfectlem1  15504  perfectlem2  15505  gausslemma2dlem0i  15567  gausslemma2dlem4  15574  lgsquad2lem1  15591  lgsquad2lem2  15592  trilpolemisumle  16014