Theorem mp3an2i 1383

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

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  mapsnend  7099  mapen  7146  mapxpen  7148  mapunen  7151  en2eleq  7547  nnledivrp  10177  xsubge0  10293  iccen  10419  fzen  10457  fldiv4lem1div2uz2  10754  frec2uzsucd  10851  seqp1g  10916  fnpfx  11463  cats1fvn  11550  seq3shft  11617  geolim2  12295  geoisum1c  12303  ntrivcvgap  12331  eflegeo  12484  sin01gt0  12545  cos01gt0  12546  3dvds  12647  gcdn0gt0  12771  uzwodc  12830  divgcdodd  12938  sqpweven  12971  2sqpwodd  12972  pythagtriplem4  13067  pythagtriplem11  13073  pythagtriplem12  13074  pythagtriplem13  13075  pythagtriplem14  13076  pcfac  13149  4sqlemffi  13195  ballotfilemfcc  13282  ballotfilemfmpn  13283  omctfn  13383  ssnnctlemct  13386  topnvalg  13654  imasmulr  13679  imasaddfnlemg  13684  gzsumsplit1r  13764  ismhm  13817  mhmex  13818  gsumvalfi  14201  prdsinvlem  14245  scaffng  14695  lss1d  14769  zringinvg  14988  psrplusgg  15118  restbasg  15318  restco  15324  lmfval  15343  cnfval  15344  cnpval  15348  upxp  15422  uptx  15424  txrest  15426  xblm  15567  bdmet  15652  bdmopn  15654  reopnap  15696  cnopnap  15761  maxcncf  15765  mincncf  15766  dvidlemap  15841  dvcj  15859  plyval  15882  plysub  15903  eflt  15925  logdivlti  16033  log2tlbndlog2  16139  perfectlem1  16197  perfectlem2  16198  gausslemma2dlem0i  16274  gausslemma2dlem4  16281  lgsquad2lem1  16298  lgsquad2lem2  16299  clwwlknon  16768  trilpolemisumle  17185