Theorem mp3an2i 1495

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

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  onnseq  8352  oeoalem  8605  oeoelem  8607  domssex2  9156  domssex  9157  sniffsupp  9392  cantnfp1lem1  9679  en2eleq  10087  en2other2  10088  infxpenc  10097  infxpenc2lem1  10098  mappwen  10191  dfac12lem2  10223  ackbij1b  10316  fin23lem26  10403  ttukeylem5  10591  gchac  10766  wunex2  10823  00id  11485  nngt1ne1  12367  gtndiv  12776  nn01to3  13068  rpnnen1lem2  13105  nnledivrp  13234  xrre3  13301  max0sub  13326  xsubge0  13391  xrub  13442  bernneq  14373  faclbnd6  14443  bc0k  14455  brfi1indALT  14655  revpfxsfxrev  14917  wrdlen2i  15093  01sqrexlem5  15413  01sqrexlem7  15415  sqreulem  15527  0.999...  16050  bpoly3  16224  fsumcube  16226  cos2t  16346  cos2tsin  16347  sin01gt0  16358  cos01gt0  16359  absefib  16366  efieq1re  16367  3dvds  16501  nno  16552  gcdcllem3  16671  gcdn0gt0  16690  divgcdodd  16886  pythagtriplem4  16997  pythagtriplem11  17003  pythagtriplem12  17004  pythagtriplem13  17005  pythagtriplem14  17006  pcfac  17077  prmreclem1  17094  vdwlem12  17170  ramval  17186  ramub2  17192  prmolelcmf  17226  prmgaplcmlem2  17230  firest  17603  yonffthlem  18456  gsumval2a  18874  prdsinvlem  19259  f1otrspeq  19661  pmtrf  19669  pmtrmvd  19670  pmtrfinv  19675  gexex  20067  cnaddinv  20085  prdsmgp  20371  elmgplsm  20372  zringlpirlem1  21768  zringinvg  21771  pzriprnglem10  21796  frgpcyg  21879  redvr  21923  frlmphllem  22086  frlmup4  22107  evls1val  22638  evls1sca  22641  smadiadetlem1  22977  smadiadetlem3lem0  22980  smadiadet  22985  d0mat2pmat  23056  chpmat0d  23152  neiptoptop  23449  upxp  23942  uptx  23944  pt1hmeo  24125  tgpconncompeqg  24431  qustgplem  24440  cnextucn  24621  psmetge0  24631  xmetge0  24663  xbln0  24733  tmsxpsval2  24858  metustid  24873  icopnfcld  25086  iocmnfcld  25087  ioo2blex  25113  tgioo  25115  blcvx  25117  xrsmopn  25132  recld2  25134  metdcn2  25159  cnmptre  25248  icchmeo  25262  cnheiborlem  25275  cnheibor  25276  lebnumii  25287  phtpyco2  25311  pi1xfrf  25374  pi1xfr  25376  pi1xfrcnvlem  25377  pi1xfrcnv  25378  pi1coghm  25382  ehleudisval  25740  ovolmge0  25798  ovolctb2  25813  nulmbl2  25857  unmbl  25858  ioombl1lem4  25882  ovolioo  25889  uniioombllem2  25904  uniioombllem4  25907  uniioombllem5  25908  uniioombllem6  25909  opnmbllem  25922  volcn  25927  i1fadd  26016  itg1addlem2  26018  i1fres  26026  itgle  26130  itgsplitioo  26158  ellimc3  26199  limcflflem  26200  limcflf  26201  limcmo  26202  limcres  26206  limciun  26214  perfdvf  26223  dvidlem  26235  dvnres  26251  dvlipcn  26314  dv11cn  26321  lhop2  26335  dvcnvrelem2  26338  tdeglem4  26378  plysub  26538  coeeulem  26543  plydiveu  26619  vieta1lem2  26634  plyexmo  26636  aaliou2b  26668  taylfval  26686  psercn  26753  pserdvlem2  26755  pserdv  26756  logdivlti  26948  efopnlem2  26985  acoscos  27221  xrlimcnp  27296  efrlim  27297  lgamucov  27365  basellem9  27416  perfectlem1  27556  perfectlem2  27557  lgsqrlem4  27676  gausslemma2dlem4  27696  lgsquad2lem1  27711  lgsquad2lem2  27712  dchrisum0lem1  27843  pntlem3  27936  pntleml  27938  qrngdiv  27951  flt4lem7  27989  nna4b4nsq  27990  nosupbday  28062  noinfbday  28077  noetainflem4  28097  madebdaylemlrcut  28285  oniso  28657  pw2divscan4d  28830  bdayfinbndlem1  28853  ttgcontlem1  29462  brbtwn2  29483  colinearalglem4  29487  ax5seglem1  29506  axcontlem4  29545  axcontlem7  29548  wlkp1lem3  30254  wlkp1lem7  30258  wlkp1lem8  30259  pthdlem1  30352  conngrv2edg  30796  mptiffisupp  33286  0mplrim  34146  psrgsum  34180  esplyfv1  34201  esplyfv  34202  esplyfval3  34204  txomap  34466  rmulccn  34560  weexenwe  35756  cvxpconn  36007  cvxsconn  36008  cvmlift2lem10  36077  knoppcnlem10  37368  itg2gt0cn  38594  resubeqsub  43482  omabs2  44334  nadd2rabex  44388  enrelmap  44997  k0004lem3  45149  sineq0ALT  45919  xlimconst  46835  evenwodadd  47911  cjnpoly  47939  2ltceilhalf  48402  2timesltsqm1  48449  odz2prm2pw  48648  fmtno4prmfac  48657  lighneallem3  48692  lighneallem4a  48693  lighneallem4  48695  gpg3kgrtriexlem3  49183  fllog2  49680  2arymptfv  49762  prelrrx2b  49826  rrxsphere  49860  2sphere  49861  line2  49864  line2x  49866  line2y  49867