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

Theorem ad4antr 731
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 729 . 2  |-  ( ( ( ( ph  /\  ch )  /\  th )  /\  ta )  ->  ps )
32adantr 465 1  |-  ( ( ( ( ( ph  /\ 
ch )  /\  th )  /\  ta )  /\  et )  ->  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:  ad5antr  733  prdsval  14710  catass  14941  catpropd  14965  cidpropd  14966  subccocl  15072  funcco  15098  natpropd  15203  fucpropd  15204  prfval  15326  xpcpropd  15335  acsfiindd  15664  scmatscm  18810  cpmatmcllem  19014  mptcoe1matfsupp  19098  mp2pm2mplem4  19105  chpdmatlem2  19135  chfacfisf  19150  chfacfisfcpmat  19151  neitr  19475  hauscmplem  19700  trcfilu  20560  cfilucfilOLD  20835  cfilucfil  20836  restmetu  20853  metucnOLD  20854  metucn  20855  cnheibor  21218  dvlip2  22159  tgifscgr  23656  tgcgrxfr  23665  tgbtwnconn1lem3  23716  tgbtwnconn1  23717  legtrd  23731  legtri3  23732  legso  23740  tglndim0  23751  tglinethru  23758  tglnpt2  23762  colline  23771  perpneq  23827  isperp2  23828  footex  23831  mideulem  23841  mideu  23842  lmieu  23855  f1otrg  23878  eupatrl  24672  3cyclfrgra  24719  2spot0  24769  numclwlk2lem2f1o  24810  omndmul2  27392  isarchi3  27421  archirngz  27423  qtophaus  27665  esumcst  27739  oms0  27934  eulerpartlemgvv  27983  signsply0  28176  signstfvneq0  28197  lgamucov  28248  cvmlift3lem2  28433  mblfinlem3  29658  mblfinlem4  29659  itg2addnclem2  29672  itg2gt0cn  29675  ftc1cnnc  29694  ftc1anc  29703  nn0prpwlem  29745  sstotbnd2  29901  pell1234qrdich  30429  pell14qrdich  30437  pell1qrgap  30442  climrec  31173  climsuse  31178  limcrecl  31199  limclner  31221  icccncfext  31254  mndpsuppss  32063  ply1mulgsumlem2  32086  lcfl8  36317
  Copyright terms: Public domain W3C validator