Theorem mp3an2i 1494

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 401  df-3an 1104

This theorem is used by:  onnseq  8329  oeoalem  8580  oeoelem  8582  domssex2  9123  domssex  9124  sniffsupp  9358  cantnfp1lem1  9645  en2eleq  9999  en2other2  10000  infxpenc  10009  infxpenc2lem1  10010  mappwen  10103  dfac12lem2  10135  ackbij1b  10228  fin23lem26  10315  ttukeylem5  10503  gchac  10672  wunex2  10729  00id  11391  nngt1ne1  12271  gtndiv  12679  nn01to3  12971  rpnnen1lem2  13007  nnledivrp  13136  xrre3  13203  max0sub  13228  xsubge0  13293  xrub  13344  bernneq  14272  faclbnd6  14342  bc0k  14354  brfi1indALT  14554  wrdlen2i  14986  01sqrexlem5  15304  01sqrexlem7  15306  sqreulem  15418  0.999...  15942  bpoly3  16118  fsumcube  16120  cos2t  16240  cos2tsin  16241  sin01gt0  16252  cos01gt0  16253  absefib  16260  efieq1re  16261  3dvds  16395  nno  16446  gcdcllem3  16565  gcdn0gt0  16582  divgcdodd  16775  pythagtriplem4  16885  pythagtriplem11  16891  pythagtriplem12  16892  pythagtriplem13  16893  pythagtriplem14  16894  pcfac  16965  prmreclem1  16982  vdwlem12  17058  ramval  17074  ramub2  17080  prmolelcmf  17114  prmgaplcmlem2  17118  firest  17491  yonffthlem  18344  gsumval2a  18749  prdsinvlem  19121  f1otrspeq  19523  pmtrf  19531  pmtrmvd  19532  pmtrfinv  19537  gexex  19929  cnaddinv  19947  prdsmgp  20233  elmgplsm  20234  zringlpirlem1  21623  zringinvg  21626  pzriprnglem10  21651  frgpcyg  21734  redvr  21778  frlmphllem  21941  frlmup4  21962  evls1val  22491  evls1sca  22494  smadiadetlem1  22830  smadiadetlem3lem0  22833  smadiadet  22838  d0mat2pmat  22906  chpmat0d  23002  neiptoptop  23299  upxp  23791  uptx  23793  pt1hmeo  23974  tgpconncompeqg  24280  qustgplem  24289  cnextucn  24470  psmetge0  24480  xmetge0  24512  xbln0  24582  tmsxpsval2  24707  metustid  24722  icopnfcld  24935  iocmnfcld  24936  ioo2blex  24962  tgioo  24964  blcvx  24966  xrsmopn  24981  recld2  24983  metdcn2  25008  cnmptre  25097  icchmeo  25111  cnheiborlem  25124  cnheibor  25125  lebnumii  25136  phtpyco2  25160  pi1xfrf  25223  pi1xfr  25225  pi1xfrcnvlem  25226  pi1xfrcnv  25227  pi1coghm  25231  ehleudisval  25589  ovolmge0  25647  ovolctb2  25662  nulmbl2  25706  unmbl  25707  ioombl1lem4  25731  ovolioo  25738  uniioombllem2  25753  uniioombllem4  25756  uniioombllem5  25757  uniioombllem6  25758  opnmbllem  25771  volcn  25776  i1fadd  25865  itg1addlem2  25867  i1fres  25875  itgle  25980  itgsplitioo  26008  ellimc3  26049  limcflflem  26050  limcflf  26051  limcmo  26052  limcres  26056  limciun  26064  perfdvf  26073  dvidlem  26085  dvnres  26101  dvlipcn  26164  dv11cn  26171  lhop2  26185  dvcnvrelem2  26188  tdeglem4  26228  plysub  26387  coeeulem  26392  plydiveu  26470  vieta1lem2  26483  plyexmo  26485  aaliou2b  26515  taylfval  26533  psercn  26600  pserdvlem2  26602  pserdv  26603  logdivlti  26796  efopnlem2  26833  acoscos  27069  xrlimcnp  27144  efrlim  27145  lgamucov  27213  basellem9  27264  perfectlem1  27404  perfectlem2  27405  lgsqrlem4  27524  gausslemma2dlem4  27544  lgsquad2lem1  27559  lgsquad2lem2  27560  dchrisum0lem1  27691  pntlem3  27784  pntleml  27786  qrngdiv  27799  nosupbday  27880  noinfbday  27895  noetainflem4  27915  madebdaylemlrcut  28103  oniso  28475  pw2divscan4d  28648  bdayfinbndlem1  28671  ttgcontlem1  29245  brbtwn2  29266  colinearalglem4  29270  ax5seglem1  29289  axcontlem4  29328  axcontlem7  29331  wlkp1lem3  30034  wlkp1lem7  30038  wlkp1lem8  30039  pthdlem1  30126  conngrv2edg  30557  mptiffisupp  33049  0mplrim  33913  psrgsum  33947  esplyfv1  33968  esplyfv  33969  esplyfval3  33971  txomap  34233  rmulccn  34327  revpfxsfxrev  35615  cvxpconn  35742  cvxsconn  35743  cvmlift2lem10  35812  knoppcnlem10  37119  itg2gt0cn  38354  resubeqsub  43219  flt4lem7  43419  nna4b4nsq  43420  omabs2  44087  nadd2rabex  44141  enrelmap  44751  k0004lem3  44903  sineq0ALT  45673  xlimconst  46567  2ltceilhalf  48097  2timesltsqm1  48144  odz2prm2pw  48343  fmtno4prmfac  48352  lighneallem3  48387  lighneallem4a  48388  lighneallem4  48390  gpg3kgrtriexlem3  48878  fllog2  49376  2arymptfv  49458  prelrrx2b  49522  rrxsphere  49556  2sphere  49557  line2  49560  line2x  49562  line2y  49563