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  tfrlem1  7047  prdsval  14834  catass  15065  catpropd  15086  cidpropd  15087  subccocl  15193  funcco  15219  natpropd  15324  fucpropd  15325  prfval  15447  xpcpropd  15456  acsfiindd  15786  mhmmnd  16171  scmatscm  18993  cpmatmcllem  19197  mptcoe1matfsupp  19281  mp2pm2mplem4  19288  chpdmatlem2  19318  chfacfisf  19333  chfacfisfcpmat  19334  neitr  19659  hauscmplem  19884  trcfilu  20775  cfilucfilOLD  21050  cfilucfil  21051  restmetu  21068  metucnOLD  21069  metucn  21070  cnheibor  21433  dvlip2  22374  tgifscgr  23878  tgbtwnconn1  23940  legtrd  23954  legtri3  23955  legso  23963  tglndim0  23987  tglinethru  23994  tglnpt2  23999  colline  24008  perpneq  24069  isperp2  24070  footex  24073  opphllem  24087  midex  24089  opphllem3  24099  opphllem5  24101  opphllem6  24102  opphl  24103  lnopp2hpgb  24110  hpgerlem  24112  lmieu  24128  f1otrg  24152  eupatrl  24946  3cyclfrgra  24993  2spot0  25042  numclwlk2lem2f1o  25083  omndmul2  27680  isarchi3  27709  archirngz  27711  qtophaus  27817  esumcst  28049  oms0  28244  eulerpartlemgvv  28293  signsply0  28486  signstfvneq0  28507  lgamucov  28558  cvmlift3lem2  28743  mblfinlem3  30029  mblfinlem4  30030  itg2addnclem2  30043  itg2gt0cn  30046  ftc1cnnc  30065  ftc1anc  30074  nn0prpwlem  30116  sstotbnd2  30246  pell1234qrdich  30773  pell14qrdich  30781  pell1qrgap  30786  pellfundex  30798  cvgdvgrat  31170  climrec  31563  climsuse  31568  limcrecl  31589  fperdvper  31669  dvnprodlem2  31698  etransclem35  32006  2zlidl  32567  mndpsuppss  32834  ply1mulgsumlem2  32857  lcfl8  37104
  Copyright terms: Public domain W3C validator