MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mp3an2i Structured version   Visualization version   GIF version

Theorem mp3an2i 1467
Description: mp3an 1462 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
StepHypRef Expression
1 mp3an2i.2 . 2 (𝜓𝜒)
2 mp3an2i.3 . 2 (𝜓𝜃)
3 mp3an2i.1 . . 3 𝜑
4 mp3an2i.4 . . 3 ((𝜑𝜒𝜃) → 𝜏)
53, 4mp3an1 1449 . 2 ((𝜒𝜃) → 𝜏)
61, 2, 5syl2anc 585 1 (𝜓𝜏)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1088
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 398  df-3an 1090
This theorem is referenced by:  wfrlem17OLD  8272  onnseq  8291  oeoalem  8544  oeoelem  8546  domssex2  9082  domssex  9083  dif1enOLD  9107  sniffsupp  9337  cantnfp1lem1  9615  en2eleq  9945  en2other2  9946  infxpenc  9955  infxpenc2lem1  9956  mappwen  10049  dfac12lem2  10081  ackbij1b  10176  fin23lem26  10262  ttukeylem5  10450  gchac  10618  wunex2  10675  00id  11331  nngt1ne1  12183  gtndiv  12581  nn01to3  12867  rpnnen1lem2  12903  nnledivrp  13028  xrre3  13091  max0sub  13116  xsubge0  13181  xrub  13232  bernneq  14133  faclbnd6  14200  bc0k  14212  brfi1indALT  14400  wrdlen2i  14832  01sqrexlem5  15132  01sqrexlem7  15134  sqreulem  15245  0.999...  15767  bpoly3  15942  fsumcube  15944  cos2t  16061  cos2tsin  16062  sin01gt0  16073  cos01gt0  16074  absefib  16081  efieq1re  16082  3dvds  16214  nno  16265  gcdcllem3  16382  gcdn0gt0  16399  divgcdodd  16587  pythagtriplem4  16692  pythagtriplem11  16698  pythagtriplem12  16699  pythagtriplem13  16700  pythagtriplem14  16701  pcfac  16772  prmreclem1  16789  vdwlem12  16865  ramval  16881  ramub2  16887  prmolelcmf  16921  prmgaplcmlem2  16925  firest  17315  yonffthlem  18172  gsumval2a  18541  prdsinvlem  18857  f1otrspeq  19230  pmtrf  19238  pmtrmvd  19239  pmtrfinv  19244  gexex  19632  cnaddinv  19650  prdsmgp  20035  zringlpirlem1  20886  zringinvg  20889  frgpcyg  20983  redvr  21024  frlmphllem  21189  frlmup4  21210  evls1val  21689  evls1sca  21692  smadiadetlem1  22014  smadiadetlem3lem0  22017  smadiadet  22022  d0mat2pmat  22090  chpmat0d  22186  neiptoptop  22485  upxp  22977  uptx  22979  pt1hmeo  23160  tgpconncompeqg  23466  qustgplem  23475  cnextucn  23658  psmetge0  23668  xmetge0  23700  xbln0  23770  tmsxpsval2  23898  metustid  23913  icopnfcld  24134  iocmnfcld  24135  ioo2blex  24160  tgioo  24162  blcvx  24164  xrsmopn  24178  recld2  24180  metdcn2  24205  cnmptre  24293  icchmeo  24307  cnheiborlem  24320  cnheibor  24321  lebnumii  24332  phtpyco2  24356  pi1xfrf  24419  pi1xfr  24421  pi1xfrcnvlem  24422  pi1xfrcnv  24423  pi1coghm  24427  ehleudisval  24786  ovolmge0  24844  ovolctb2  24859  nulmbl2  24903  unmbl  24904  ioombl1lem4  24928  ovolioo  24935  uniioombllem2  24950  uniioombllem4  24953  uniioombllem5  24954  uniioombllem6  24955  opnmbllem  24968  volcn  24973  i1fadd  25062  itg1addlem2  25064  i1fres  25073  itgle  25177  itgsplitioo  25205  ellimc3  25246  limcflflem  25247  limcflf  25248  limcmo  25249  limcres  25253  limciun  25261  perfdvf  25270  dvidlem  25282  dvnres  25298  dvlipcn  25361  dv11cn  25368  lhop2  25382  dvcnvrelem2  25385  tdeglem4  25427  plysub  25583  coeeulem  25588  plydiveu  25661  vieta1lem2  25674  plyexmo  25676  aaliou2b  25704  taylfval  25721  psercn  25788  pserdvlem2  25790  pserdv  25791  logdivlti  25978  efopnlem2  26015  acoscos  26246  xrlimcnp  26321  efrlim  26322  lgamucov  26390  basellem9  26441  perfectlem1  26580  perfectlem2  26581  lgsqrlem4  26700  gausslemma2dlem4  26720  lgsquad2lem1  26735  lgsquad2lem2  26736  dchrisum0lem1  26867  pntlem3  26960  pntleml  26962  qrngdiv  26975  nosupbday  27056  noinfbday  27071  noetainflem4  27091  madebdaylemlrcut  27231  ttgcontlem1  27836  brbtwn2  27857  colinearalglem4  27861  ax5seglem1  27880  axcontlem4  27919  axcontlem7  27922  wlkp1lem3  28626  wlkp1lem7  28630  wlkp1lem8  28631  pthdlem1  28717  conngrv2edg  29142  elringlsm  32177  txomap  32418  revpfxsfxrev  33712  cvmlift2lem10  33909  itg2gt0cn  36136  resubeqsub  40901  flt4lem7  41000  nna4b4nsq  41001  omabs2  41668  enrelmap  42276  k0004lem3  42428  sineq0ALT  43226  xlimconst  44073  odz2prm2pw  45762  fmtno4prmfac  45771  lighneallem3  45806  lighneallem4a  45807  lighneallem4  45809  fllog2  46661  2arymptfv  46743  prelrrx2b  46807  rrxsphere  46841  2sphere  46842  line2  46845  line2x  46847  line2y  46848
  Copyright terms: Public domain W3C validator