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  8279  oeoalem  8527  oeoelem  8529  domssex2  9070  domssex  9071  sniffsupp  9308  cantnfp1lem1  9594  en2eleq  9925  en2other2  9926  infxpenc  9935  infxpenc2lem1  9936  mappwen  10029  dfac12lem2  10062  ackbij1b  10155  fin23lem26  10242  ttukeylem5  10430  gchac  10599  wunex2  10656  00id  11316  nngt1ne1  12201  gtndiv  12601  nn01to3  12886  rpnnen1lem2  12922  nnledivrp  13051  xrre3  13118  max0sub  13143  xsubge0  13208  xrub  13259  bernneq  14186  faclbnd6  14256  bc0k  14268  brfi1indALT  14467  wrdlen2i  14899  01sqrexlem5  15203  01sqrexlem7  15205  sqreulem  15317  0.999...  15841  bpoly3  16018  fsumcube  16020  cos2t  16140  cos2tsin  16141  sin01gt0  16152  cos01gt0  16153  absefib  16160  efieq1re  16161  3dvds  16295  nno  16346  gcdcllem3  16465  gcdn0gt0  16482  divgcdodd  16675  pythagtriplem4  16785  pythagtriplem11  16791  pythagtriplem12  16792  pythagtriplem13  16793  pythagtriplem14  16794  pcfac  16865  prmreclem1  16882  vdwlem12  16958  ramval  16974  ramub2  16980  prmolelcmf  17014  prmgaplcmlem2  17018  firest  17390  yonffthlem  18243  gsumval2a  18648  prdsinvlem  19020  f1otrspeq  19417  pmtrf  19425  pmtrmvd  19426  pmtrfinv  19431  gexex  19823  cnaddinv  19841  prdsmgp  20127  zringlpirlem1  21456  zringinvg  21459  pzriprnglem10  21484  frgpcyg  21567  redvr  21611  frlmphllem  21774  frlmup4  21795  evls1val  22299  evls1sca  22302  smadiadetlem1  22641  smadiadetlem3lem0  22644  smadiadet  22649  d0mat2pmat  22717  chpmat0d  22813  neiptoptop  23110  upxp  23602  uptx  23604  pt1hmeo  23785  tgpconncompeqg  24091  qustgplem  24100  cnextucn  24281  psmetge0  24291  xmetge0  24323  xbln0  24393  tmsxpsval2  24518  metustid  24533  icopnfcld  24746  iocmnfcld  24747  ioo2blex  24773  tgioo  24775  blcvx  24777  xrsmopn  24792  recld2  24794  metdcn2  24819  cnmptre  24908  icchmeo  24922  cnheiborlem  24935  cnheibor  24936  lebnumii  24947  phtpyco2  24971  pi1xfrf  25034  pi1xfr  25036  pi1xfrcnvlem  25037  pi1xfrcnv  25038  pi1coghm  25042  ehleudisval  25400  ovolmge0  25458  ovolctb2  25473  nulmbl2  25517  unmbl  25518  ioombl1lem4  25542  ovolioo  25549  uniioombllem2  25564  uniioombllem4  25567  uniioombllem5  25568  uniioombllem6  25569  opnmbllem  25582  volcn  25587  i1fadd  25676  itg1addlem2  25678  i1fres  25686  itgle  25791  itgsplitioo  25819  ellimc3  25860  limcflflem  25861  limcflf  25862  limcmo  25863  limcres  25867  limciun  25875  perfdvf  25884  dvidlem  25896  dvnres  25912  dvlipcn  25975  dv11cn  25982  lhop2  25996  dvcnvrelem2  25999  tdeglem4  26039  plysub  26198  coeeulem  26203  plydiveu  26279  vieta1lem2  26292  plyexmo  26294  aaliou2b  26322  taylfval  26339  psercn  26408  pserdvlem2  26410  pserdv  26411  logdivlti  26601  efopnlem2  26638  acoscos  26874  xrlimcnp  26949  efrlim  26950  efrlimOLD  26951  lgamucov  27019  basellem9  27070  perfectlem1  27210  perfectlem2  27211  lgsqrlem4  27330  gausslemma2dlem4  27350  lgsquad2lem1  27365  lgsquad2lem2  27366  dchrisum0lem1  27497  pntlem3  27590  pntleml  27592  qrngdiv  27605  nosupbday  27687  noinfbday  27702  noetainflem4  27722  madebdaylemlrcut  27909  oniso  28281  pw2divscan4d  28454  bdayfinbndlem1  28477  ttgcontlem1  28971  brbtwn2  28992  colinearalglem4  28996  ax5seglem1  29015  axcontlem4  29054  axcontlem7  29057  wlkp1lem3  29761  wlkp1lem7  29765  wlkp1lem8  29766  pthdlem1  29853  conngrv2edg  30284  mptiffisupp  32785  elringlsm  33472  psrgsum  33711  esplyfv1  33732  esplyfv  33733  esplyfval3  33735  txomap  33998  rmulccn  34092  revpfxsfxrev  35318  cvxpconn  35444  cvxsconn  35445  cvmlift2lem10  35514  knoppcnlem10  36782  itg2gt0cn  38016  resubeqsub  42882  flt4lem7  43112  nna4b4nsq  43113  omabs2  43784  nadd2rabex  43838  enrelmap  44448  k0004lem3  44600  sineq0ALT  45387  xlimconst  46277  2ltceilhalf  47798  2timesltsqm1  47845  odz2prm2pw  48044  fmtno4prmfac  48053  lighneallem3  48088  lighneallem4a  48089  lighneallem4  48091  gpg3kgrtriexlem3  48579  fllog2  49062  2arymptfv  49144  prelrrx2b  49208  rrxsphere  49242  2sphere  49243  line2  49246  line2x  49248  line2y  49249