Theorem mp3an2i 1489

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

Syntax hints:   → wi 4   ∧ w3a 1099

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 209  df-an 400  df-3an 1101

This theorem is referenced by:  onnseq  8317  oeoalem  8568  oeoelem  8570  domssex2  9111  domssex  9112  sniffsupp  9348  cantnfp1lem1  9635  en2eleq  9966  en2other2  9967  infxpenc  9976  infxpenc2lem1  9977  mappwen  10070  dfac12lem2  10103  ackbij1b  10196  fin23lem26  10284  ttukeylem5  10472  gchac  10641  wunex2  10698  00id  11360  nngt1ne1  12244  gtndiv  12652  nn01to3  12944  rpnnen1lem2  12980  nnledivrp  13109  xrre3  13176  max0sub  13201  xsubge0  13266  xrub  13317  bernneq  14244  faclbnd6  14314  bc0k  14326  brfi1indALT  14525  wrdlen2i  14957  01sqrexlem5  15275  01sqrexlem7  15277  sqreulem  15389  0.999...  15913  bpoly3  16090  fsumcube  16092  cos2t  16212  cos2tsin  16213  sin01gt0  16224  cos01gt0  16225  absefib  16232  efieq1re  16233  3dvds  16367  nno  16418  gcdcllem3  16537  gcdn0gt0  16554  divgcdodd  16747  pythagtriplem4  16857  pythagtriplem11  16863  pythagtriplem12  16864  pythagtriplem13  16865  pythagtriplem14  16866  pcfac  16937  prmreclem1  16954  vdwlem12  17030  ramval  17046  ramub2  17052  prmolelcmf  17086  prmgaplcmlem2  17090  firest  17463  yonffthlem  18316  gsumval2a  18721  prdsinvlem  19093  f1otrspeq  19489  pmtrf  19497  pmtrmvd  19498  pmtrfinv  19503  gexex  19895  cnaddinv  19913  prdsmgp  20199  zringlpirlem1  21516  zringinvg  21519  pzriprnglem10  21544  frgpcyg  21627  redvr  21671  frlmphllem  21834  frlmup4  21855  evls1val  22385  evls1sca  22388  smadiadetlem1  22724  smadiadetlem3lem0  22727  smadiadet  22732  d0mat2pmat  22800  chpmat0d  22896  neiptoptop  23193  upxp  23685  uptx  23687  pt1hmeo  23868  tgpconncompeqg  24174  qustgplem  24183  cnextucn  24364  psmetge0  24374  xmetge0  24406  xbln0  24476  tmsxpsval2  24601  metustid  24616  icopnfcld  24829  iocmnfcld  24830  ioo2blex  24856  tgioo  24858  blcvx  24860  xrsmopn  24875  recld2  24877  metdcn2  24902  cnmptre  24991  icchmeo  25005  cnheiborlem  25018  cnheibor  25019  lebnumii  25030  phtpyco2  25054  pi1xfrf  25117  pi1xfr  25119  pi1xfrcnvlem  25120  pi1xfrcnv  25121  pi1coghm  25125  ehleudisval  25483  ovolmge0  25541  ovolctb2  25556  nulmbl2  25600  unmbl  25601  ioombl1lem4  25625  ovolioo  25632  uniioombllem2  25647  uniioombllem4  25650  uniioombllem5  25651  uniioombllem6  25652  opnmbllem  25665  volcn  25670  i1fadd  25759  itg1addlem2  25761  i1fres  25769  itgle  25874  itgsplitioo  25902  ellimc3  25943  limcflflem  25944  limcflf  25945  limcmo  25946  limcres  25950  limciun  25958  perfdvf  25967  dvidlem  25979  dvnres  25995  dvlipcn  26058  dv11cn  26065  lhop2  26079  dvcnvrelem2  26082  tdeglem4  26122  plysub  26281  coeeulem  26286  plydiveu  26364  vieta1lem2  26377  plyexmo  26379  aaliou2b  26407  taylfval  26424  psercn  26491  pserdvlem2  26493  pserdv  26494  logdivlti  26687  efopnlem2  26724  acoscos  26960  xrlimcnp  27035  efrlim  27036  lgamucov  27104  basellem9  27155  perfectlem1  27295  perfectlem2  27296  lgsqrlem4  27415  gausslemma2dlem4  27435  lgsquad2lem1  27450  lgsquad2lem2  27451  dchrisum0lem1  27582  pntlem3  27675  pntleml  27677  qrngdiv  27690  nosupbday  27771  noinfbday  27786  noetainflem4  27806  madebdaylemlrcut  27994  oniso  28366  pw2divscan4d  28539  bdayfinbndlem1  28562  ttgcontlem1  29087  brbtwn2  29108  colinearalglem4  29112  ax5seglem1  29131  axcontlem4  29170  axcontlem7  29173  wlkp1lem3  29876  wlkp1lem7  29880  wlkp1lem8  29881  pthdlem1  29968  conngrv2edg  30399  mptiffisupp  32897  elringlsm  33581  0mplrim  33813  psrgsum  33847  esplyfv1  33868  esplyfv  33869  esplyfval3  33871  txomap  34133  rmulccn  34227  revpfxsfxrev  35470  cvxpconn  35597  cvxsconn  35598  cvmlift2lem10  35667  knoppcnlem10  36945  itg2gt0cn  38179  resubeqsub  43044  flt4lem7  43246  nna4b4nsq  43247  omabs2  43914  nadd2rabex  43968  enrelmap  44578  k0004lem3  44730  sineq0ALT  45517  xlimconst  46404  2ltceilhalf  47931  2timesltsqm1  47978  odz2prm2pw  48177  fmtno4prmfac  48186  lighneallem3  48221  lighneallem4a  48222  lighneallem4  48224  gpg3kgrtriexlem3  48712  fllog2  49195  2arymptfv  49277  prelrrx2b  49341  rrxsphere  49375  2sphere  49376  line2  49379  line2x  49381  line2y  49382