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  8290  oeoalem  8537  oeoelem  8539  domssex2  9078  domssex  9079  dif1enOLD  9103  sniffsupp  9327  cantnfp1lem1  9609  en2eleq  9939  en2other2  9940  infxpenc  9949  infxpenc2lem1  9950  mappwen  10043  dfac12lem2  10076  ackbij1b  10169  fin23lem26  10256  ttukeylem5  10444  gchac  10612  wunex2  10669  00id  11327  nngt1ne1  12193  gtndiv  12589  nn01to3  12878  rpnnen1lem2  12914  nnledivrp  13043  xrre3  13109  max0sub  13134  xsubge0  13199  xrub  13250  bernneq  14172  faclbnd6  14242  bc0k  14254  brfi1indALT  14453  wrdlen2i  14885  01sqrexlem5  15189  01sqrexlem7  15191  sqreulem  15303  0.999...  15824  bpoly3  16001  fsumcube  16003  cos2t  16123  cos2tsin  16124  sin01gt0  16135  cos01gt0  16136  absefib  16143  efieq1re  16144  3dvds  16278  nno  16329  gcdcllem3  16448  gcdn0gt0  16465  divgcdodd  16657  pythagtriplem4  16767  pythagtriplem11  16773  pythagtriplem12  16774  pythagtriplem13  16775  pythagtriplem14  16776  pcfac  16847  prmreclem1  16864  vdwlem12  16940  ramval  16956  ramub2  16962  prmolelcmf  16996  prmgaplcmlem2  17000  firest  17372  yonffthlem  18224  gsumval2a  18595  prdsinvlem  18964  f1otrspeq  19362  pmtrf  19370  pmtrmvd  19371  pmtrfinv  19376  gexex  19768  cnaddinv  19786  prdsmgp  20072  zringlpirlem1  21405  zringinvg  21408  pzriprnglem10  21433  frgpcyg  21516  redvr  21560  frlmphllem  21723  frlmup4  21744  evls1val  22241  evls1sca  22244  smadiadetlem1  22583  smadiadetlem3lem0  22586  smadiadet  22591  d0mat2pmat  22659  chpmat0d  22755  neiptoptop  23052  upxp  23544  uptx  23546  pt1hmeo  23727  tgpconncompeqg  24033  qustgplem  24042  cnextucn  24224  psmetge0  24234  xmetge0  24266  xbln0  24336  tmsxpsval2  24461  metustid  24476  icopnfcld  24689  iocmnfcld  24690  ioo2blex  24716  tgioo  24718  blcvx  24720  xrsmopn  24735  recld2  24737  metdcn2  24762  cnmptre  24855  icchmeo  24872  icchmeoOLD  24873  cnheiborlem  24887  cnheibor  24888  lebnumii  24899  phtpyco2  24923  pi1xfrf  24987  pi1xfr  24989  pi1xfrcnvlem  24990  pi1xfrcnv  24991  pi1coghm  24995  ehleudisval  25353  ovolmge0  25412  ovolctb2  25427  nulmbl2  25471  unmbl  25472  ioombl1lem4  25496  ovolioo  25503  uniioombllem2  25518  uniioombllem4  25521  uniioombllem5  25522  uniioombllem6  25523  opnmbllem  25536  volcn  25541  i1fadd  25630  itg1addlem2  25632  i1fres  25640  itgle  25745  itgsplitioo  25773  ellimc3  25814  limcflflem  25815  limcflf  25816  limcmo  25817  limcres  25821  limciun  25829  perfdvf  25838  dvidlem  25850  dvnres  25867  dvlipcn  25933  dv11cn  25940  lhop2  25954  dvcnvrelem2  25957  tdeglem4  25999  plysub  26158  coeeulem  26163  plydiveu  26240  vieta1lem2  26253  plyexmo  26255  aaliou2b  26283  taylfval  26300  psercn  26370  pserdvlem2  26372  pserdv  26373  logdivlti  26563  efopnlem2  26600  acoscos  26837  xrlimcnp  26912  efrlim  26913  efrlimOLD  26914  lgamucov  26982  basellem9  27033  perfectlem1  27174  perfectlem2  27175  lgsqrlem4  27294  gausslemma2dlem4  27314  lgsquad2lem1  27329  lgsquad2lem2  27330  dchrisum0lem1  27461  pntlem3  27554  pntleml  27556  qrngdiv  27569  nosupbday  27651  noinfbday  27666  noetainflem4  27686  madebdaylemlrcut  27849  onsiso  28210  pw2divscan4d  28372  ttgcontlem1  28866  brbtwn2  28886  colinearalglem4  28890  ax5seglem1  28909  axcontlem4  28948  axcontlem7  28951  wlkp1lem3  29655  wlkp1lem7  29659  wlkp1lem8  29660  pthdlem1  29747  conngrv2edg  30175  mptiffisupp  32667  elringlsm  33358  txomap  33818  rmulccn  33912  revpfxsfxrev  35097  cvxpconn  35223  cvxsconn  35224  cvmlift2lem10  35293  knoppcnlem10  36484  itg2gt0cn  37663  resubeqsub  42412  flt4lem7  42641  nna4b4nsq  42642  omabs2  43315  nadd2rabex  43369  enrelmap  43980  k0004lem3  44132  sineq0ALT  44920  xlimconst  45817  2ltceilhalf  47323  odz2prm2pw  47558  fmtno4prmfac  47567  lighneallem3  47602  lighneallem4a  47603  lighneallem4  47605  gpg3kgrtriexlem3  48070  fllog2  48551  2arymptfv  48633  prelrrx2b  48697  rrxsphere  48731  2sphere  48732  line2  48735  line2x  48737  line2y  48738