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

Theorem mp3an2i 1459
Description: mp3an 1454 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 1441 . 2 ((𝜒𝜃) → 𝜏)
61, 2, 5syl2anc 584 1 (𝜓𝜏)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1081
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 208  df-an 397  df-3an 1083
This theorem is referenced by:  wfrlem17  7967  onnseq  7977  oeoalem  8217  oeoelem  8219  domssex2  8671  domssex  8672  sniffsupp  8867  cantnfp1lem1  9135  en2eleq  9428  en2other2  9429  infxpenc  9438  infxpenc2lem1  9439  mappwen  9532  dfac12lem2  9564  ackbij1b  9655  fin23lem26  9741  ttukeylem5  9929  gchac  10097  wunex2  10154  00id  10809  fiminreOLD  11584  nngt1ne1  11660  gtndiv  12053  nn01to3  12335  rpnnen1lem2  12371  nnledivrp  12496  xrre3  12559  max0sub  12584  xsubge0  12649  xrub  12700  bernneq  13585  faclbnd6  13654  bc0k  13666  wrdlen2i  14299  sqrlem5  14601  sqrlem7  14603  sqreulem  14714  0.999...  15232  bpoly3  15407  fsumcube  15409  cos2t  15526  cos2tsin  15527  sin01gt0  15538  cos01gt0  15539  absefib  15546  efieq1re  15547  3dvds  15675  nno  15728  gcdcllem3  15845  gcdn0gt0  15861  divgcdodd  16049  pythagtriplem4  16151  pythagtriplem11  16157  pythagtriplem12  16158  pythagtriplem13  16159  pythagtriplem14  16160  pcfac  16230  prmreclem1  16247  vdwlem12  16323  ramval  16339  ramub2  16345  prmolelcmf  16379  prmgaplcmlem2  16383  firest  16701  yonffthlem  17527  gsumval2a  17890  prdsinvlem  18153  f1otrspeq  18511  pmtrf  18519  pmtrmvd  18520  pmtrfinv  18525  gexex  18909  cnaddinv  18927  prdsmgp  19296  opsrtoslem2  20200  evls1val  20418  evls1sca  20421  zringlpirlem1  20566  zringinvg  20569  frgpcyg  20655  redvr  20696  frlmphllem  20859  frlmup4  20880  smadiadetlem1  21206  smadiadetlem3lem0  21209  smadiadet  21214  d0mat2pmat  21281  chpmat0d  21377  neiptoptop  21674  upxp  22166  uptx  22168  pt1hmeo  22349  tgpconncompeqg  22654  qustgplem  22663  cnextucn  22846  psmetge0  22856  xmetge0  22888  xbln0  22958  tmsxpsval2  23083  metustid  23098  icopnfcld  23310  iocmnfcld  23311  ioo2blex  23336  tgioo  23338  blcvx  23340  xrsmopn  23354  recld2  23356  metdcn2  23381  cnmptre  23465  icchmeo  23479  cnheiborlem  23492  cnheibor  23493  lebnumii  23504  phtpyco2  23528  pi1xfrf  23591  pi1xfr  23593  pi1xfrcnvlem  23594  pi1xfrcnv  23595  pi1coghm  23599  ehleudisval  23956  ovolmge0  24012  ovolctb2  24027  nulmbl2  24071  unmbl  24072  ioombl1lem4  24096  ovolioo  24103  uniioombllem2  24118  uniioombllem4  24121  uniioombllem5  24122  uniioombllem6  24123  opnmbllem  24136  volcn  24141  i1fadd  24230  itg1addlem2  24232  i1fres  24240  itgle  24344  itgsplitioo  24372  ellimc3  24411  limcflflem  24412  limcflf  24413  limcmo  24414  limcres  24418  limciun  24426  perfdvf  24435  dvidlem  24447  dvnres  24462  dvlipcn  24525  dv11cn  24532  lhop2  24546  dvcnvrelem2  24549  plysub  24743  coeeulem  24748  plydiveu  24821  vieta1lem2  24834  plyexmo  24836  aaliou2b  24864  taylfval  24881  psercn  24948  pserdvlem2  24950  pserdv  24951  logdivlti  25135  efopnlem2  25172  acoscos  25403  xrlimcnp  25479  efrlim  25480  lgamucov  25548  basellem9  25599  perfectlem1  25738  perfectlem2  25739  lgsqrlem4  25858  gausslemma2dlem4  25878  lgsquad2lem1  25893  lgsquad2lem2  25894  dchrisum0lem1  26025  pntlem3  26118  pntleml  26120  qrngdiv  26133  ttgcontlem1  26604  brbtwn2  26624  colinearalglem4  26628  ax5seglem1  26647  axcontlem4  26686  axcontlem7  26689  wlkp1lem3  27390  wlkp1lem7  27394  wlkp1lem8  27395  pthdlem1  27480  conngrv2edg  27907  txomap  31003  revpfxsfxrev  32265  cvmlift2lem10  32462  nosupbday  33108  itg2gt0cn  34833  enrelmap  40227  k0004lem3  40383  sineq0ALT  41155  xlimconst  41990  odz2prm2pw  43576  fmtno4prmfac  43585  lighneallem3  43623  lighneallem4a  43624  lighneallem4  43626  fllog2  44530  prelrrx2b  44603  rrxsphere  44637  2sphere  44638  line2  44641  line2x  44643  line2y  44644
  Copyright terms: Public domain W3C validator