Theorem mp3an2i 1468

Description: mp3an 1463 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 1450	. 2 ⊢ ((𝜒 ∧ 𝜃) → 𝜏)
6	1, 2, 5	syl2anc 584	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:  wfrlem17OLD  8365  onnseq  8384  oeoalem  8634  oeoelem  8636  domssex2  9177  domssex  9178  dif1enOLD  9202  sniffsupp  9440  cantnfp1lem1  9718  en2eleq  10048  en2other2  10049  infxpenc  10058  infxpenc2lem1  10059  mappwen  10152  dfac12lem2  10185  ackbij1b  10278  fin23lem26  10365  ttukeylem5  10553  gchac  10721  wunex2  10778  00id  11436  nngt1ne1  12295  gtndiv  12695  nn01to3  12983  rpnnen1lem2  13019  nnledivrp  13147  xrre3  13213  max0sub  13238  xsubge0  13303  xrub  13354  bernneq  14268  faclbnd6  14338  bc0k  14350  brfi1indALT  14549  wrdlen2i  14981  01sqrexlem5  15285  01sqrexlem7  15287  sqreulem  15398  0.999...  15917  bpoly3  16094  fsumcube  16096  cos2t  16214  cos2tsin  16215  sin01gt0  16226  cos01gt0  16227  absefib  16234  efieq1re  16235  3dvds  16368  nno  16419  gcdcllem3  16538  gcdn0gt0  16555  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  17477  yonffthlem  18327  gsumval2a  18698  prdsinvlem  19067  f1otrspeq  19465  pmtrf  19473  pmtrmvd  19474  pmtrfinv  19479  gexex  19871  cnaddinv  19889  prdsmgp  20148  zringlpirlem1  21473  zringinvg  21476  pzriprnglem10  21501  frgpcyg  21592  redvr  21635  frlmphllem  21800  frlmup4  21821  evls1val  22324  evls1sca  22327  smadiadetlem1  22668  smadiadetlem3lem0  22671  smadiadet  22676  d0mat2pmat  22744  chpmat0d  22840  neiptoptop  23139  upxp  23631  uptx  23633  pt1hmeo  23814  tgpconncompeqg  24120  qustgplem  24129  cnextucn  24312  psmetge0  24322  xmetge0  24354  xbln0  24424  tmsxpsval2  24552  metustid  24567  icopnfcld  24788  iocmnfcld  24789  ioo2blex  24815  tgioo  24817  blcvx  24819  xrsmopn  24834  recld2  24836  metdcn2  24861  cnmptre  24954  icchmeo  24971  icchmeoOLD  24972  cnheiborlem  24986  cnheibor  24987  lebnumii  24998  phtpyco2  25022  pi1xfrf  25086  pi1xfr  25088  pi1xfrcnvlem  25089  pi1xfrcnv  25090  pi1coghm  25094  ehleudisval  25453  ovolmge0  25512  ovolctb2  25527  nulmbl2  25571  unmbl  25572  ioombl1lem4  25596  ovolioo  25603  uniioombllem2  25618  uniioombllem4  25621  uniioombllem5  25622  uniioombllem6  25623  opnmbllem  25636  volcn  25641  i1fadd  25730  itg1addlem2  25732  i1fres  25740  itgle  25845  itgsplitioo  25873  ellimc3  25914  limcflflem  25915  limcflf  25916  limcmo  25917  limcres  25921  limciun  25929  perfdvf  25938  dvidlem  25950  dvnres  25967  dvlipcn  26033  dv11cn  26040  lhop2  26054  dvcnvrelem2  26057  tdeglem4  26099  plysub  26258  coeeulem  26263  plydiveu  26340  vieta1lem2  26353  plyexmo  26355  aaliou2b  26383  taylfval  26400  psercn  26470  pserdvlem2  26472  pserdv  26473  logdivlti  26662  efopnlem2  26699  acoscos  26936  xrlimcnp  27011  efrlim  27012  efrlimOLD  27013  lgamucov  27081  basellem9  27132  perfectlem1  27273  perfectlem2  27274  lgsqrlem4  27393  gausslemma2dlem4  27413  lgsquad2lem1  27428  lgsquad2lem2  27429  dchrisum0lem1  27560  pntlem3  27653  pntleml  27655  qrngdiv  27668  nosupbday  27750  noinfbday  27765  noetainflem4  27785  madebdaylemlrcut  27937  ttgcontlem1  28899  brbtwn2  28920  colinearalglem4  28924  ax5seglem1  28943  axcontlem4  28982  axcontlem7  28985  wlkp1lem3  29693  wlkp1lem7  29697  wlkp1lem8  29698  pthdlem1  29786  conngrv2edg  30214  mptiffisupp  32702  elringlsm  33421  txomap  33833  rmulccn  33927  revpfxsfxrev  35121  cvxpconn  35247  cvxsconn  35248  cvmlift2lem10  35317  knoppcnlem10  36503  itg2gt0cn  37682  resubeqsub  42459  flt4lem7  42669  nna4b4nsq  42670  omabs2  43345  nadd2rabex  43399  enrelmap  44010  k0004lem3  44162  sineq0ALT  44957  xlimconst  45840  odz2prm2pw  47550  fmtno4prmfac  47559  lighneallem3  47594  lighneallem4a  47595  lighneallem4  47597  2ltceilhalf  48015  gpg3kgrtriexlem3  48041  fllog2  48489  2arymptfv  48571  prelrrx2b  48635  rrxsphere  48669  2sphere  48670  line2  48673  line2x  48675  line2y  48676