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  7049  prdsval  15296  catass  15535  catpropd  15557  cidpropd  15558  subccocl  15693  funcco  15719  natpropd  15824  fucpropd  15825  initoeu2lem1  15852  prfval  16027  xpcpropd  16036  acsfiindd  16366  mhmmnd  16751  scmatscm  19480  cpmatmcllem  19684  mptcoe1matfsupp  19768  mp2pm2mplem4  19775  chpdmatlem2  19805  chfacfisf  19820  chfacfisfcpmat  19821  neitr  20138  hauscmplem  20363  trcfilu  21251  cfilucfil  21516  restmetu  21527  metucn  21528  cnheibor  21925  dvlip2  22889  lgamucov  23905  tgifscgr  24495  iscgrglt  24501  tgbtwnconn1  24562  legtrd  24576  legtri3  24577  legso  24586  hlcgrex  24603  tglndim0  24616  tglinethru  24623  tglnpt2  24628  colline  24636  perpneq  24701  isperp2  24702  footex  24705  opphllem  24719  midex  24721  opphllem3  24733  opphllem5  24735  opphllem6  24736  opphl  24738  outpasch  24739  hlpasch  24740  lnopp2hpgb  24747  hpgerlem  24749  lmieu  24768  trgcopy  24788  cgrahl  24810  acopy  24816  inaghl  24823  cgrg3col4  24826  f1otrg  24843  eupatrl  25638  3cyclfrgra  25685  2spot0  25734  numclwlk2lem2f1o  25775  omndmul2  28426  isarchi3  28455  archirngz  28457  psgnfzto1stlem  28565  qtophaus  28615  esumcst  28836  sigapildsys  28936  oms0  29077  omssubadd  29080  oms0OLD  29081  omssubaddOLD  29084  carsgclctunlem3  29104  eulerpartlemgvv  29161  signsply0  29392  signstfvneq0  29413  cvmlift3lem2  29995  nn0prpwlem  30927  mblfinlem3  31886  mblfinlem4  31887  itg2addnclem2  31901  itg2gt0cn  31904  ftc1cnnc  31923  ftc1anc  31932  sstotbnd2  32013  lcfl8  34982  pell1234qrdich  35620  pell14qrdich  35628  pell1qrgap  35633  pellfundex  35647  cvgdvgrat  36575  climrec  37564  climsuse  37570  limcrecl  37592  fperdvper  37673  dvnprodlem2  37705  etransclem35  38017  iccpartgt  38554  2zlidl  39535  mndpsuppss  39759  ply1mulgsumlem2  39782  nn0sumshdiglemA  40033
  Copyright terms: Public domain W3C validator