Theorem mp3an2i 1469

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

Syntax hints:   → wi 4   ∧ w3a 1087

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1089

This theorem is referenced by:  onnseq  8273  oeoalem  8521  oeoelem  8523  domssex2  9064  domssex  9065  sniffsupp  9302  cantnfp1lem1  9588  en2eleq  9919  en2other2  9920  infxpenc  9929  infxpenc2lem1  9930  mappwen  10023  dfac12lem2  10056  ackbij1b  10149  fin23lem26  10236  ttukeylem5  10424  gchac  10593  wunex2  10650  00id  11310  nngt1ne1  12195  gtndiv  12595  nn01to3  12880  rpnnen1lem2  12916  nnledivrp  13045  xrre3  13112  max0sub  13137  xsubge0  13202  xrub  13253  bernneq  14180  faclbnd6  14250  bc0k  14262  brfi1indALT  14461  wrdlen2i  14893  01sqrexlem5  15197  01sqrexlem7  15199  sqreulem  15311  0.999...  15835  bpoly3  16012  fsumcube  16014  cos2t  16134  cos2tsin  16135  sin01gt0  16146  cos01gt0  16147  absefib  16154  efieq1re  16155  3dvds  16289  nno  16340  gcdcllem3  16459  gcdn0gt0  16476  divgcdodd  16669  pythagtriplem4  16779  pythagtriplem11  16785  pythagtriplem12  16786  pythagtriplem13  16787  pythagtriplem14  16788  pcfac  16859  prmreclem1  16876  vdwlem12  16952  ramval  16968  ramub2  16974  prmolelcmf  17008  prmgaplcmlem2  17012  firest  17384  yonffthlem  18237  gsumval2a  18642  prdsinvlem  19014  f1otrspeq  19411  pmtrf  19419  pmtrmvd  19420  pmtrfinv  19425  gexex  19817  cnaddinv  19835  prdsmgp  20121  zringlpirlem1  21431  zringinvg  21434  pzriprnglem10  21459  frgpcyg  21542  redvr  21586  frlmphllem  21749  frlmup4  21770  evls1val  22273  evls1sca  22276  smadiadetlem1  22615  smadiadetlem3lem0  22618  smadiadet  22623  d0mat2pmat  22691  chpmat0d  22787  neiptoptop  23084  upxp  23576  uptx  23578  pt1hmeo  23759  tgpconncompeqg  24065  qustgplem  24074  cnextucn  24255  psmetge0  24265  xmetge0  24297  xbln0  24367  tmsxpsval2  24492  metustid  24507  icopnfcld  24720  iocmnfcld  24721  ioo2blex  24747  tgioo  24749  blcvx  24751  xrsmopn  24766  recld2  24768  metdcn2  24793  cnmptre  24882  icchmeo  24896  cnheiborlem  24909  cnheibor  24910  lebnumii  24921  phtpyco2  24945  pi1xfrf  25008  pi1xfr  25010  pi1xfrcnvlem  25011  pi1xfrcnv  25012  pi1coghm  25016  ehleudisval  25374  ovolmge0  25432  ovolctb2  25447  nulmbl2  25491  unmbl  25492  ioombl1lem4  25516  ovolioo  25523  uniioombllem2  25538  uniioombllem4  25541  uniioombllem5  25542  uniioombllem6  25543  opnmbllem  25556  volcn  25561  i1fadd  25650  itg1addlem2  25652  i1fres  25660  itgle  25765  itgsplitioo  25793  ellimc3  25834  limcflflem  25835  limcflf  25836  limcmo  25837  limcres  25841  limciun  25849  perfdvf  25858  dvidlem  25870  dvnres  25886  dvlipcn  25949  dv11cn  25956  lhop2  25970  dvcnvrelem2  25973  tdeglem4  26013  plysub  26172  coeeulem  26177  plydiveu  26252  vieta1lem2  26265  plyexmo  26267  aaliou2b  26295  taylfval  26312  psercn  26379  pserdvlem2  26381  pserdv  26382  logdivlti  26572  efopnlem2  26609  acoscos  26845  xrlimcnp  26920  efrlim  26921  lgamucov  26989  basellem9  27040  perfectlem1  27180  perfectlem2  27181  lgsqrlem4  27300  gausslemma2dlem4  27320  lgsquad2lem1  27335  lgsquad2lem2  27336  dchrisum0lem1  27467  pntlem3  27560  pntleml  27562  qrngdiv  27575  nosupbday  27657  noinfbday  27672  noetainflem4  27692  madebdaylemlrcut  27879  oniso  28251  pw2divscan4d  28424  bdayfinbndlem1  28447  ttgcontlem1  28941  brbtwn2  28962  colinearalglem4  28966  ax5seglem1  28985  axcontlem4  29024  axcontlem7  29027  wlkp1lem3  29730  wlkp1lem7  29734  wlkp1lem8  29735  pthdlem1  29822  conngrv2edg  30253  mptiffisupp  32754  elringlsm  33441  psrgsum  33680  esplyfv1  33701  esplyfv  33702  esplyfval3  33704  txomap  33966  rmulccn  34060  revpfxsfxrev  35286  cvxpconn  35412  cvxsconn  35413  cvmlift2lem10  35482  knoppcnlem10  36750  itg2gt0cn  37984  resubeqsub  42850  flt4lem7  43080  nna4b4nsq  43081  omabs2  43748  nadd2rabex  43802  enrelmap  44412  k0004lem3  44564  sineq0ALT  45351  xlimconst  46241  2ltceilhalf  47768  2timesltsqm1  47815  odz2prm2pw  48014  fmtno4prmfac  48023  lighneallem3  48058  lighneallem4a  48059  lighneallem4  48061  gpg3kgrtriexlem3  48549  fllog2  49032  2arymptfv  49114  prelrrx2b  49178  rrxsphere  49212  2sphere  49213  line2  49216  line2x  49218  line2y  49219