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

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

Proof of Theorem ad4antr
StepHypRef Expression
1 ad2ant.1 . . 3  |-  ( ph  ->  ps )
21ad3antrrr 734 . 2  |-  ( ( ( ( ph  /\  ch )  /\  th )  /\  ta )  ->  ps )
32adantr 466 1  |-  ( ( ( ( ( ph  /\ 
ch )  /\  th )  /\  ta )  /\  et )  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370
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 188  df-an 372
This theorem is referenced by:  ad5antr  738  tfrlem1  7102  prdsval  15312  catass  15543  catpropd  15565  cidpropd  15566  subccocl  15701  funcco  15727  natpropd  15832  fucpropd  15833  initoeu2lem1  15860  prfval  16035  xpcpropd  16044  acsfiindd  16374  mhmmnd  16759  scmatscm  19469  cpmatmcllem  19673  mptcoe1matfsupp  19757  mp2pm2mplem4  19764  chpdmatlem2  19794  chfacfisf  19809  chfacfisfcpmat  19810  neitr  20127  hauscmplem  20352  trcfilu  21240  cfilucfil  21505  restmetu  21516  metucn  21517  cnheibor  21879  dvlip2  22824  lgamucov  23828  tgifscgr  24416  tgbtwnconn1  24480  legtrd  24494  legtri3  24495  legso  24504  hlcgrex  24520  tglndim0  24533  tglinethru  24540  tglnpt2  24545  colline  24554  perpneq  24616  isperp2  24617  footex  24620  opphllem  24634  midex  24636  opphllem3  24648  opphllem5  24650  opphllem6  24651  opphl  24653  outpasch  24654  lnopp2hpgb  24661  hpgerlem  24663  lmieu  24682  trgcopy  24702  cgrahl  24723  acopy  24727  f1otrg  24747  eupatrl  25541  3cyclfrgra  25588  2spot0  25637  numclwlk2lem2f1o  25678  omndmul2  28313  isarchi3  28342  archirngz  28344  psgnfzto1stlem  28452  qtophaus  28502  esumcst  28723  sigapildsys  28823  oms0  28958  omssubadd  28961  carsgclctunlem3  28981  eulerpartlemgvv  29035  signsply0  29228  signstfvneq0  29249  cvmlift3lem2  29831  nn0prpwlem  30763  mblfinlem3  31682  mblfinlem4  31683  itg2addnclem2  31697  itg2gt0cn  31700  ftc1cnnc  31719  ftc1anc  31728  sstotbnd2  31809  lcfl8  34778  pell1234qrdich  35414  pell14qrdich  35422  pell1qrgap  35427  pellfundex  35439  cvgdvgrat  36298  climrec  37252  climsuse  37258  limcrecl  37280  fperdvper  37361  dvnprodlem2  37390  etransclem35  37700  iccpartgt  38130  2zlidl  38691  mndpsuppss  38915  ply1mulgsumlem2  38938  nn0sumshdiglemA  39190
  Copyright terms: Public domain W3C validator