MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ad3antlr Structured version   Unicode version

Theorem ad3antlr 725
Description: Deduction adding three conjuncts to antecedent. (Contributed by Mario Carneiro, 5-Jan-2017.)
Hypothesis
Ref Expression
ad2ant.1  |-  ( ph  ->  ps )
Assertion
Ref Expression
ad3antlr  |-  ( ( ( ( ch  /\  ph )  /\  th )  /\  ta )  ->  ps )

Proof of Theorem ad3antlr
StepHypRef Expression
1 ad2ant.1 . . 3  |-  ( ph  ->  ps )
21ad2antlr 721 . 2  |-  ( ( ( ch  /\  ph )  /\  th )  ->  ps )
32adantr 462 1  |-  ( ( ( ( ch  /\  ph )  /\  th )  /\  ta )  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369
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 185  df-an 371
This theorem is referenced by:  ad4antlr  727  oaass  6996  undom  7395  acndom2  8220  infxp  8380  isf32lem2  8519  ttukeylem3  8676  gchina  8862  r1limwun  8899  difreicc  11413  ssfzo12bi  11618  o1of2  13086  rlimsqzlem  13122  isprm5  13794  ramval  14065  mreexexlem4d  14581  acsfn  14593  gasubg  15813  psgndiflemB  17930  psgndiflemA  17931  mdetf  18306  restcld  18676  cnpnei  18768  iscncl  18773  cncls  18778  cnntr  18779  1stcfb  18949  2ndcdisj  18960  txlly  19109  fbflim  19449  fclsbas  19494  nmoi  20207  fgcfil  20682  equivcau  20711  cmetcuspOLD  20765  cmetcusp  20766  itg2cnlem1  21139  iblss  21182  lgsqr  22628  axcontlem2  23130  fargshiftfva  23444  constr3trllem2  23456  eupatrl  23508  blocnilem  24123  mdslmd3i  25655  fgreu  25909  resf1o  25949  omndmul2  26092  gsumpropd2lem  26161  pstmxmet  26244  lmdvg  26303  oddpwdc  26651  sgnmul  26839  signstres  26890  cvmlift2lem12  27117  ltflcei  28328  lxflflp1  28330  heicant  28335  mblfinlem2  28338  mblfinlem3  28339  mblfinlem4  28340  ismblfin  28341  itg2addnclem  28352  itg2addnclem2  28353  itg2addnclem3  28354  itg2addnc  28355  itg2gt0cn  28356  ftc1cnnc  28375  ftc1anclem5  28380  ftc1anclem6  28381  ftc1anclem7  28382  ftc1anclem8  28383  ftc1anc  28384  elicc3  28421  nn0prpwlem  28426  neibastop2  28491  neibastop3  28492  nnubfi  28555  nninfnub  28556  diophren  29061  irrapxlem2  29073  irrapxlem4  29075  wepwsolem  29303  wallispilem3  29771  wwlktovf1  30161  usgra2wlkspth  30207  wlkiswwlk1  30233  wwlkext2clwwlk  30374  clwwisshclwwlem  30379  frgra2v  30500  vdn1frgrav2  30527  vdgn1frgrav2  30528  frgrawopreg  30551  2spotiundisj  30564  usgreg2spot  30569  numclwlk1lem2f1  30596  numclwlk2lem2f1o  30607  scmatsubcl  30750  snlindsntor  30829  linepsubN  33084  lhpmatb  33363  cdlemf2  33894  diaglbN  34388  diaintclN  34391  dibglbN  34499  dibintclN  34500  dihlsscpre  34567  dihglblem5aN  34625  dihglblem2aN  34626  dih1dimatlem  34662
  Copyright terms: Public domain W3C validator