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

Theorem ad3antlr 730
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 726 . 2  |-  ( ( ( ch  /\  ph )  /\  th )  ->  ps )
32adantr 465 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  732  oaass  7210  undom  7605  acndom2  8434  infxp  8594  isf32lem2  8733  ttukeylem3  8890  gchina  9076  r1limwun  9113  difreicc  11651  ssfzo12bi  11874  flflp1  11911  wwlktovf1  12857  o1of2  13397  rlimsqzlem  13433  isprm5  14111  ramval  14384  mreexexlem4d  14901  acsfn  14913  gsumpropd2lem  15824  gasubg  16142  psgndiflemB  18419  psgndiflemA  18420  mdetf  18880  cpmatacl  19000  cpmatinvcl  19001  mat2pmatf1  19013  mp2pm2mplem4  19093  chfacffsupp  19140  restcld  19455  cnpnei  19547  iscncl  19552  cncls  19557  cnntr  19558  1stcfb  19728  2ndcdisj  19739  txlly  19888  fbflim  20228  fclsbas  20273  nmoi  20986  fgcfil  21461  equivcau  21490  cmetcuspOLD  21544  cmetcusp  21545  itg2cnlem1  21919  iblss  21962  lgsqr  23365  axcontlem2  23960  usgra2wlkspth  24313  fargshiftfva  24331  constr3trllem2  24343  wlkiswwlk1  24382  wwlkext2clwwlk  24495  clwwisshclwwlem  24498  eupatrl  24660  frgra2v  24691  vdn1frgrav2  24718  vdgn1frgrav2  24719  frgrawopreg  24742  2spotiundisj  24755  usgreg2spot  24760  numclwlk1lem2f1  24787  numclwlk2lem2f1o  24798  blocnilem  25411  mdslmd3i  26943  fgreu  27201  resf1o  27241  omndmul2  27380  fimaproj  27515  pstmxmet  27528  lmdvg  27587  oddpwdc  27949  sgnmul  28137  signstres  28188  cvmlift2lem12  28415  ltflcei  29636  heicant  29642  mblfinlem2  29645  mblfinlem3  29646  mblfinlem4  29647  ismblfin  29648  itg2addnclem  29659  itg2addnclem2  29660  itg2addnclem3  29661  itg2addnc  29662  itg2gt0cn  29663  ftc1cnnc  29682  ftc1anclem5  29687  ftc1anclem6  29688  ftc1anclem7  29689  ftc1anclem8  29690  ftc1anc  29691  elicc3  29728  nn0prpwlem  29733  neibastop2  29798  neibastop3  29799  nnubfi  29862  nninfnub  29863  diophren  30367  irrapxlem2  30379  irrapxlem4  30381  wepwsolem  30607  prmunb2  30810  lcmgcdlem  30828  icccncfext  31242  iblcncfioo  31312  wallispilem3  31383  fourierdlem12  31435  fourierdlem50  31473  fourierdlem65  31488  fourierdlem77  31500  ply1mulgsumlem2  32077  snlindsntor  32162  linepsubN  34557  lhpmatb  34836  cdlemf2  35367  diaglbN  35861  diaintclN  35864  dibglbN  35972  dibintclN  35973  dihlsscpre  36040  dihglblem5aN  36098  dihglblem2aN  36099  dih1dimatlem  36135
  Copyright terms: Public domain W3C validator