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

Theorem ad3antlr 728
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 724 . 2  |-  ( ( ( ch  /\  ph )  /\  th )  ->  ps )
32adantr 463 1  |-  ( ( ( ( ch  /\  ph )  /\  th )  /\  ta )  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367
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 369
This theorem is referenced by:  ad4antlr  730  tfrlem1  6963  oaass  7128  undom  7524  acndom2  8348  infxp  8508  isf32lem2  8647  ttukeylem3  8804  gchina  8988  r1limwun  9025  difreicc  11573  ssfzo12bi  11806  flflp1  11843  ccatcl  12502  wwlktovf1  12806  o1of2  13437  rlimsqzlem  13473  isprm5  14255  ramval  14528  mreexexlem4d  15054  acsfn  15066  gsumpropd2lem  16017  gasubg  16457  psgndiflemB  18727  psgndiflemA  18728  mdetf  19182  cpmatacl  19302  cpmatinvcl  19303  mat2pmatf1  19315  mp2pm2mplem4  19395  chfacffsupp  19442  restcld  19759  cnpnei  19851  iscncl  19856  cncls  19861  cnntr  19862  1stcfb  20031  2ndcdisj  20042  txlly  20222  fbflim  20562  fclsbas  20607  nmoi  21320  fgcfil  21795  equivcau  21824  cmetcuspOLD  21878  cmetcusp  21879  itg2cnlem1  22253  iblss  22296  lgsqr  23738  axcontlem2  24389  usgra2wlkspth  24742  fargshiftfva  24760  constr3trllem2  24772  wlkiswwlk1  24811  wwlkext2clwwlk  24924  clwwisshclwwlem  24927  eupatrl  25089  frgra2v  25120  vdn1frgrav2  25146  vdgn1frgrav2  25147  frgrawopreg  25170  2spotiundisj  25183  usgreg2spot  25188  numclwlk1lem2f1  25215  numclwlk2lem2f1o  25226  blocnilem  25836  mdslmd3i  27367  foresf1o  27521  fgreu  27659  resf1o  27703  omndmul2  27855  fimaproj  27990  locfinreflem  27997  cmpcref  28007  pstmxmet  28030  lmdvg  28089  carsgclctunlem3  28447  oddpwdc  28476  sgnmul  28664  signstres  28715  cvmlift2lem12  28948  mrsubff  29061  ltflcei  30208  heicant  30214  mblfinlem2  30217  mblfinlem3  30218  mblfinlem4  30219  ismblfin  30220  itg2addnclem  30232  itg2addnclem2  30233  itg2addnclem3  30234  itg2addnc  30235  itg2gt0cn  30236  ftc1cnnc  30255  ftc1anclem5  30260  ftc1anclem6  30261  ftc1anclem7  30262  ftc1anclem8  30263  ftc1anc  30264  elicc3  30301  nn0prpwlem  30306  neibastop2  30345  neibastop3  30346  nnubfi  30409  nninfnub  30410  diophren  30912  irrapxlem2  30924  irrapxlem4  30926  wepwsolem  31153  prmunb2  31359  cvgdvgrat  31362  lcmgcdlem  31380  icccncfext  31856  ioodvbdlimc1lem1  31894  iblcncfioo  31943  wallispilem3  32015  fourierdlem12  32067  fourierdlem34  32089  fourierdlem50  32105  fourierdlem51  32106  fourierdlem65  32120  fourierdlem77  32132  opoeALTV  32525  opeoALTV  32526  issubmgm2  32796  uzlidlring  32935  2zrngmmgm  32952  cznrng  32963  ply1mulgsumlem2  33187  snlindsntor  33272  elbigo2  33373  nn0sumshdiglemA  33440  linepsubN  35889  lhpmatb  36168  cdlemf2  36701  diaglbN  37195  diaintclN  37198  dibglbN  37306  dibintclN  37307  dihlsscpre  37374  dihglblem5aN  37432  dihglblem2aN  37433  dih1dimatlem  37469
  Copyright terms: Public domain W3C validator