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 1086

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 1088

This theorem is referenced by:  onnseq  8291  oeoalem  8538  oeoelem  8540  domssex2  9079  domssex  9080  dif1enOLD  9104  sniffsupp  9328  cantnfp1lem1  9610  en2eleq  9940  en2other2  9941  infxpenc  9950  infxpenc2lem1  9951  mappwen  10044  dfac12lem2  10077  ackbij1b  10170  fin23lem26  10257  ttukeylem5  10445  gchac  10613  wunex2  10670  00id  11328  nngt1ne1  12194  gtndiv  12590  nn01to3  12879  rpnnen1lem2  12915  nnledivrp  13044  xrre3  13110  max0sub  13135  xsubge0  13200  xrub  13251  bernneq  14173  faclbnd6  14243  bc0k  14255  brfi1indALT  14454  wrdlen2i  14886  01sqrexlem5  15190  01sqrexlem7  15192  sqreulem  15304  0.999...  15825  bpoly3  16002  fsumcube  16004  cos2t  16124  cos2tsin  16125  sin01gt0  16136  cos01gt0  16137  absefib  16144  efieq1re  16145  3dvds  16279  nno  16330  gcdcllem3  16449  gcdn0gt0  16466  divgcdodd  16658  pythagtriplem4  16768  pythagtriplem11  16774  pythagtriplem12  16775  pythagtriplem13  16776  pythagtriplem14  16777  pcfac  16848  prmreclem1  16865  vdwlem12  16941  ramval  16957  ramub2  16963  prmolelcmf  16997  prmgaplcmlem2  17001  firest  17373  yonffthlem  18225  gsumval2a  18596  prdsinvlem  18965  f1otrspeq  19363  pmtrf  19371  pmtrmvd  19372  pmtrfinv  19377  gexex  19769  cnaddinv  19787  prdsmgp  20073  zringlpirlem1  21406  zringinvg  21409  pzriprnglem10  21434  frgpcyg  21517  redvr  21561  frlmphllem  21724  frlmup4  21745  evls1val  22242  evls1sca  22245  smadiadetlem1  22584  smadiadetlem3lem0  22587  smadiadet  22592  d0mat2pmat  22660  chpmat0d  22756  neiptoptop  23053  upxp  23545  uptx  23547  pt1hmeo  23728  tgpconncompeqg  24034  qustgplem  24043  cnextucn  24225  psmetge0  24235  xmetge0  24267  xbln0  24337  tmsxpsval2  24462  metustid  24477  icopnfcld  24690  iocmnfcld  24691  ioo2blex  24717  tgioo  24719  blcvx  24721  xrsmopn  24736  recld2  24738  metdcn2  24763  cnmptre  24856  icchmeo  24873  icchmeoOLD  24874  cnheiborlem  24888  cnheibor  24889  lebnumii  24900  phtpyco2  24924  pi1xfrf  24988  pi1xfr  24990  pi1xfrcnvlem  24991  pi1xfrcnv  24992  pi1coghm  24996  ehleudisval  25354  ovolmge0  25413  ovolctb2  25428  nulmbl2  25472  unmbl  25473  ioombl1lem4  25497  ovolioo  25504  uniioombllem2  25519  uniioombllem4  25522  uniioombllem5  25523  uniioombllem6  25524  opnmbllem  25537  volcn  25542  i1fadd  25631  itg1addlem2  25633  i1fres  25641  itgle  25746  itgsplitioo  25774  ellimc3  25815  limcflflem  25816  limcflf  25817  limcmo  25818  limcres  25822  limciun  25830  perfdvf  25839  dvidlem  25851  dvnres  25868  dvlipcn  25934  dv11cn  25941  lhop2  25955  dvcnvrelem2  25958  tdeglem4  26000  plysub  26159  coeeulem  26164  plydiveu  26241  vieta1lem2  26254  plyexmo  26256  aaliou2b  26284  taylfval  26301  psercn  26371  pserdvlem2  26373  pserdv  26374  logdivlti  26564  efopnlem2  26601  acoscos  26838  xrlimcnp  26913  efrlim  26914  efrlimOLD  26915  lgamucov  26983  basellem9  27034  perfectlem1  27175  perfectlem2  27176  lgsqrlem4  27295  gausslemma2dlem4  27315  lgsquad2lem1  27330  lgsquad2lem2  27331  dchrisum0lem1  27462  pntlem3  27555  pntleml  27557  qrngdiv  27570  nosupbday  27652  noinfbday  27667  noetainflem4  27687  madebdaylemlrcut  27850  onsiso  28211  pw2divscan4d  28373  ttgcontlem1  28867  brbtwn2  28887  colinearalglem4  28891  ax5seglem1  28910  axcontlem4  28949  axcontlem7  28952  wlkp1lem3  29656  wlkp1lem7  29660  wlkp1lem8  29661  pthdlem1  29748  conngrv2edg  30176  mptiffisupp  32668  elringlsm  33359  txomap  33819  rmulccn  33913  revpfxsfxrev  35098  cvxpconn  35224  cvxsconn  35225  cvmlift2lem10  35294  knoppcnlem10  36485  itg2gt0cn  37664  resubeqsub  42413  flt4lem7  42642  nna4b4nsq  42643  omabs2  43316  nadd2rabex  43370  enrelmap  43981  k0004lem3  44133  sineq0ALT  44921  xlimconst  45818  2ltceilhalf  47324  odz2prm2pw  47559  fmtno4prmfac  47568  lighneallem3  47603  lighneallem4a  47604  lighneallem4  47606  gpg3kgrtriexlem3  48071  fllog2  48552  2arymptfv  48634  prelrrx2b  48698  rrxsphere  48732  2sphere  48733  line2  48736  line2x  48738  line2y  48739