Theorem mp3an2i 1465

Description: mp3an 1460 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 1447	. 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:  wfrlem17OLD  8363  onnseq  8382  oeoalem  8632  oeoelem  8634  domssex2  9175  domssex  9176  dif1enOLD  9200  sniffsupp  9437  cantnfp1lem1  9715  en2eleq  10045  en2other2  10046  infxpenc  10055  infxpenc2lem1  10056  mappwen  10149  dfac12lem2  10182  ackbij1b  10275  fin23lem26  10362  ttukeylem5  10550  gchac  10718  wunex2  10775  00id  11433  nngt1ne1  12292  gtndiv  12692  nn01to3  12980  rpnnen1lem2  13016  nnledivrp  13144  xrre3  13209  max0sub  13234  xsubge0  13299  xrub  13350  bernneq  14264  faclbnd6  14334  bc0k  14346  brfi1indALT  14545  wrdlen2i  14977  01sqrexlem5  15281  01sqrexlem7  15283  sqreulem  15394  0.999...  15913  bpoly3  16090  fsumcube  16092  cos2t  16210  cos2tsin  16211  sin01gt0  16222  cos01gt0  16223  absefib  16230  efieq1re  16231  3dvds  16364  nno  16415  gcdcllem3  16534  gcdn0gt0  16551  divgcdodd  16743  pythagtriplem4  16852  pythagtriplem11  16858  pythagtriplem12  16859  pythagtriplem13  16860  pythagtriplem14  16861  pcfac  16932  prmreclem1  16949  vdwlem12  17025  ramval  17041  ramub2  17047  prmolelcmf  17081  prmgaplcmlem2  17085  firest  17478  yonffthlem  18338  gsumval2a  18710  prdsinvlem  19079  f1otrspeq  19479  pmtrf  19487  pmtrmvd  19488  pmtrfinv  19493  gexex  19885  cnaddinv  19903  prdsmgp  20168  zringlpirlem1  21490  zringinvg  21493  pzriprnglem10  21518  frgpcyg  21609  redvr  21652  frlmphllem  21817  frlmup4  21838  evls1val  22339  evls1sca  22342  smadiadetlem1  22683  smadiadetlem3lem0  22686  smadiadet  22691  d0mat2pmat  22759  chpmat0d  22855  neiptoptop  23154  upxp  23646  uptx  23648  pt1hmeo  23829  tgpconncompeqg  24135  qustgplem  24144  cnextucn  24327  psmetge0  24337  xmetge0  24369  xbln0  24439  tmsxpsval2  24567  metustid  24582  icopnfcld  24803  iocmnfcld  24804  ioo2blex  24829  tgioo  24831  blcvx  24833  xrsmopn  24847  recld2  24849  metdcn2  24874  cnmptre  24967  icchmeo  24984  icchmeoOLD  24985  cnheiborlem  24999  cnheibor  25000  lebnumii  25011  phtpyco2  25035  pi1xfrf  25099  pi1xfr  25101  pi1xfrcnvlem  25102  pi1xfrcnv  25103  pi1coghm  25107  ehleudisval  25466  ovolmge0  25525  ovolctb2  25540  nulmbl2  25584  unmbl  25585  ioombl1lem4  25609  ovolioo  25616  uniioombllem2  25631  uniioombllem4  25634  uniioombllem5  25635  uniioombllem6  25636  opnmbllem  25649  volcn  25654  i1fadd  25743  itg1addlem2  25745  i1fres  25754  itgle  25859  itgsplitioo  25887  ellimc3  25928  limcflflem  25929  limcflf  25930  limcmo  25931  limcres  25935  limciun  25943  perfdvf  25952  dvidlem  25964  dvnres  25981  dvlipcn  26047  dv11cn  26054  lhop2  26068  dvcnvrelem2  26071  tdeglem4  26113  plysub  26272  coeeulem  26277  plydiveu  26354  vieta1lem2  26367  plyexmo  26369  aaliou2b  26397  taylfval  26414  psercn  26484  pserdvlem2  26486  pserdv  26487  logdivlti  26676  efopnlem2  26713  acoscos  26950  xrlimcnp  27025  efrlim  27026  efrlimOLD  27027  lgamucov  27095  basellem9  27146  perfectlem1  27287  perfectlem2  27288  lgsqrlem4  27407  gausslemma2dlem4  27427  lgsquad2lem1  27442  lgsquad2lem2  27443  dchrisum0lem1  27574  pntlem3  27667  pntleml  27669  qrngdiv  27682  nosupbday  27764  noinfbday  27779  noetainflem4  27799  madebdaylemlrcut  27951  ttgcontlem1  28913  brbtwn2  28934  colinearalglem4  28938  ax5seglem1  28957  axcontlem4  28996  axcontlem7  28999  wlkp1lem3  29707  wlkp1lem7  29711  wlkp1lem8  29712  pthdlem1  29798  conngrv2edg  30223  mptiffisupp  32707  elringlsm  33400  txomap  33794  rmulccn  33888  revpfxsfxrev  35099  cvxpconn  35226  cvxsconn  35227  cvmlift2lem10  35296  knoppcnlem10  36484  itg2gt0cn  37661  resubeqsub  42435  flt4lem7  42645  nna4b4nsq  42646  omabs2  43321  nadd2rabex  43375  enrelmap  43986  k0004lem3  44138  sineq0ALT  44934  xlimconst  45780  odz2prm2pw  47487  fmtno4prmfac  47496  lighneallem3  47531  lighneallem4a  47532  lighneallem4  47534  2ltceilhalf  47949  fllog2  48417  2arymptfv  48499  prelrrx2b  48563  rrxsphere  48597  2sphere  48598  line2  48601  line2x  48603  line2y  48604