Theorem mp3an2i 1464

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

Syntax hints:   → wi 4   ∧ w3a 1085

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 206  df-an 396  df-3an 1087

This theorem is referenced by:  wfrlem17OLD  8127  onnseq  8146  oeoalem  8389  oeoelem  8391  domssex2  8873  domssex  8874  dif1en  8907  sniffsupp  9089  cantnfp1lem1  9366  en2eleq  9695  en2other2  9696  infxpenc  9705  infxpenc2lem1  9706  mappwen  9799  dfac12lem2  9831  ackbij1b  9926  fin23lem26  10012  ttukeylem5  10200  gchac  10368  wunex2  10425  00id  11080  nngt1ne1  11932  gtndiv  12327  nn01to3  12610  rpnnen1lem2  12646  nnledivrp  12771  xrre3  12834  max0sub  12859  xsubge0  12924  xrub  12975  bernneq  13872  faclbnd6  13941  bc0k  13953  brfi1indALT  14142  wrdlen2i  14583  sqrlem5  14886  sqrlem7  14888  sqreulem  14999  0.999...  15521  bpoly3  15696  fsumcube  15698  cos2t  15815  cos2tsin  15816  sin01gt0  15827  cos01gt0  15828  absefib  15835  efieq1re  15836  3dvds  15968  nno  16019  gcdcllem3  16136  gcdn0gt0  16153  divgcdodd  16343  pythagtriplem4  16448  pythagtriplem11  16454  pythagtriplem12  16455  pythagtriplem13  16456  pythagtriplem14  16457  pcfac  16528  prmreclem1  16545  vdwlem12  16621  ramval  16637  ramub2  16643  prmolelcmf  16677  prmgaplcmlem2  16681  firest  17060  yonffthlem  17916  gsumval2a  18284  prdsinvlem  18599  f1otrspeq  18970  pmtrf  18978  pmtrmvd  18979  pmtrfinv  18984  gexex  19369  cnaddinv  19387  prdsmgp  19764  zringlpirlem1  20596  zringinvg  20599  frgpcyg  20693  redvr  20734  frlmphllem  20897  frlmup4  20918  evls1val  21396  evls1sca  21399  smadiadetlem1  21719  smadiadetlem3lem0  21722  smadiadet  21727  d0mat2pmat  21795  chpmat0d  21891  neiptoptop  22190  upxp  22682  uptx  22684  pt1hmeo  22865  tgpconncompeqg  23171  qustgplem  23180  cnextucn  23363  psmetge0  23373  xmetge0  23405  xbln0  23475  tmsxpsval2  23601  metustid  23616  icopnfcld  23837  iocmnfcld  23838  ioo2blex  23863  tgioo  23865  blcvx  23867  xrsmopn  23881  recld2  23883  metdcn2  23908  cnmptre  23996  icchmeo  24010  cnheiborlem  24023  cnheibor  24024  lebnumii  24035  phtpyco2  24059  pi1xfrf  24122  pi1xfr  24124  pi1xfrcnvlem  24125  pi1xfrcnv  24126  pi1coghm  24130  ehleudisval  24488  ovolmge0  24546  ovolctb2  24561  nulmbl2  24605  unmbl  24606  ioombl1lem4  24630  ovolioo  24637  uniioombllem2  24652  uniioombllem4  24655  uniioombllem5  24656  uniioombllem6  24657  opnmbllem  24670  volcn  24675  i1fadd  24764  itg1addlem2  24766  i1fres  24775  itgle  24879  itgsplitioo  24907  ellimc3  24948  limcflflem  24949  limcflf  24950  limcmo  24951  limcres  24955  limciun  24963  perfdvf  24972  dvidlem  24984  dvnres  25000  dvlipcn  25063  dv11cn  25070  lhop2  25084  dvcnvrelem2  25087  tdeglem4  25129  plysub  25285  coeeulem  25290  plydiveu  25363  vieta1lem2  25376  plyexmo  25378  aaliou2b  25406  taylfval  25423  psercn  25490  pserdvlem2  25492  pserdv  25493  logdivlti  25680  efopnlem2  25717  acoscos  25948  xrlimcnp  26023  efrlim  26024  lgamucov  26092  basellem9  26143  perfectlem1  26282  perfectlem2  26283  lgsqrlem4  26402  gausslemma2dlem4  26422  lgsquad2lem1  26437  lgsquad2lem2  26438  dchrisum0lem1  26569  pntlem3  26662  pntleml  26664  qrngdiv  26677  ttgcontlem1  27155  brbtwn2  27176  colinearalglem4  27180  ax5seglem1  27199  axcontlem4  27238  axcontlem7  27241  wlkp1lem3  27945  wlkp1lem7  27949  wlkp1lem8  27950  pthdlem1  28035  conngrv2edg  28460  elringlsm  31483  txomap  31686  revpfxsfxrev  32977  cvmlift2lem10  33174  nosupbday  33835  noinfbday  33850  noetainflem4  33870  madebdaylemlrcut  34006  itg2gt0cn  35759  resubeqsub  40332  flt4lem7  40412  nna4b4nsq  40413  enrelmap  41494  k0004lem3  41648  sineq0ALT  42446  xlimconst  43256  odz2prm2pw  44903  fmtno4prmfac  44912  lighneallem3  44947  lighneallem4a  44948  lighneallem4  44950  fllog2  45802  2arymptfv  45884  prelrrx2b  45948  rrxsphere  45982  2sphere  45983  line2  45986  line2x  45988  line2y  45989