Theorem mp3an2i 1492

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

Syntax hints:   → wi 4   ∧ w3a 1101

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 210  df-an 401  df-3an 1103

This theorem is referenced by:  onnseq  8331  oeoalem  8582  oeoelem  8584  domssex2  9125  domssex  9126  sniffsupp  9360  cantnfp1lem1  9647  en2eleq  9992  en2other2  9993  infxpenc  10002  infxpenc2lem1  10003  mappwen  10096  dfac12lem2  10128  ackbij1b  10221  fin23lem26  10309  ttukeylem5  10497  gchac  10666  wunex2  10723  00id  11385  nngt1ne1  12265  gtndiv  12673  nn01to3  12965  rpnnen1lem2  13001  nnledivrp  13130  xrre3  13197  max0sub  13222  xsubge0  13287  xrub  13338  bernneq  14265  faclbnd6  14335  bc0k  14347  brfi1indALT  14547  wrdlen2i  14979  01sqrexlem5  15297  01sqrexlem7  15299  sqreulem  15411  0.999...  15935  bpoly3  16112  fsumcube  16114  cos2t  16234  cos2tsin  16235  sin01gt0  16246  cos01gt0  16247  absefib  16254  efieq1re  16255  3dvds  16389  nno  16440  gcdcllem3  16559  gcdn0gt0  16576  divgcdodd  16769  pythagtriplem4  16879  pythagtriplem11  16885  pythagtriplem12  16886  pythagtriplem13  16887  pythagtriplem14  16888  pcfac  16959  prmreclem1  16976  vdwlem12  17052  ramval  17068  ramub2  17074  prmolelcmf  17108  prmgaplcmlem2  17112  firest  17485  yonffthlem  18338  gsumval2a  18743  prdsinvlem  19115  f1otrspeq  19517  pmtrf  19525  pmtrmvd  19526  pmtrfinv  19531  gexex  19923  cnaddinv  19941  prdsmgp  20227  elmgplsm  20228  zringlpirlem1  21581  zringinvg  21584  pzriprnglem10  21609  frgpcyg  21692  redvr  21736  frlmphllem  21899  frlmup4  21920  evls1val  22449  evls1sca  22452  smadiadetlem1  22788  smadiadetlem3lem0  22791  smadiadet  22796  d0mat2pmat  22864  chpmat0d  22960  neiptoptop  23257  upxp  23749  uptx  23751  pt1hmeo  23932  tgpconncompeqg  24238  qustgplem  24247  cnextucn  24428  psmetge0  24438  xmetge0  24470  xbln0  24540  tmsxpsval2  24665  metustid  24680  icopnfcld  24893  iocmnfcld  24894  ioo2blex  24920  tgioo  24922  blcvx  24924  xrsmopn  24939  recld2  24941  metdcn2  24966  cnmptre  25055  icchmeo  25069  cnheiborlem  25082  cnheibor  25083  lebnumii  25094  phtpyco2  25118  pi1xfrf  25181  pi1xfr  25183  pi1xfrcnvlem  25184  pi1xfrcnv  25185  pi1coghm  25189  ehleudisval  25547  ovolmge0  25605  ovolctb2  25620  nulmbl2  25664  unmbl  25665  ioombl1lem4  25689  ovolioo  25696  uniioombllem2  25711  uniioombllem4  25714  uniioombllem5  25715  uniioombllem6  25716  opnmbllem  25729  volcn  25734  i1fadd  25823  itg1addlem2  25825  i1fres  25833  itgle  25938  itgsplitioo  25966  ellimc3  26007  limcflflem  26008  limcflf  26009  limcmo  26010  limcres  26014  limciun  26022  perfdvf  26031  dvidlem  26043  dvnres  26059  dvlipcn  26122  dv11cn  26129  lhop2  26143  dvcnvrelem2  26146  tdeglem4  26186  plysub  26345  coeeulem  26350  plydiveu  26428  vieta1lem2  26441  plyexmo  26443  aaliou2b  26471  taylfval  26488  psercn  26555  pserdvlem2  26557  pserdv  26558  logdivlti  26751  efopnlem2  26788  acoscos  27024  xrlimcnp  27099  efrlim  27100  lgamucov  27168  basellem9  27219  perfectlem1  27359  perfectlem2  27360  lgsqrlem4  27479  gausslemma2dlem4  27499  lgsquad2lem1  27514  lgsquad2lem2  27515  dchrisum0lem1  27646  pntlem3  27739  pntleml  27741  qrngdiv  27754  nosupbday  27835  noinfbday  27850  noetainflem4  27870  madebdaylemlrcut  28058  oniso  28430  pw2divscan4d  28603  bdayfinbndlem1  28626  ttgcontlem1  29175  brbtwn2  29196  colinearalglem4  29200  ax5seglem1  29219  axcontlem4  29258  axcontlem7  29261  wlkp1lem3  29964  wlkp1lem7  29968  wlkp1lem8  29969  pthdlem1  30056  conngrv2edg  30487  mptiffisupp  32979  0mplrim  33849  psrgsum  33883  esplyfv1  33904  esplyfv  33905  esplyfval3  33907  txomap  34169  rmulccn  34263  revpfxsfxrev  35540  cvxpconn  35667  cvxsconn  35668  cvmlift2lem10  35737  knoppcnlem10  37014  itg2gt0cn  38249  resubeqsub  43116  flt4lem7  43318  nna4b4nsq  43319  omabs2  43986  nadd2rabex  44040  enrelmap  44650  k0004lem3  44802  sineq0ALT  45572  xlimconst  46466  2ltceilhalf  47993  2timesltsqm1  48040  odz2prm2pw  48239  fmtno4prmfac  48248  lighneallem3  48283  lighneallem4a  48284  lighneallem4  48286  gpg3kgrtriexlem3  48774  fllog2  49268  2arymptfv  49350  prelrrx2b  49414  rrxsphere  49448  2sphere  49449  line2  49452  line2x  49454  line2y  49455