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  14391  catass  14622  catpropd  14646  cidpropd  14647  subccocl  14753  funcco  14779  natpropd  14884  fucpropd  14885  prfval  15007  xpcpropd  15016  acsfiindd  15345  neitr  18782  hauscmplem  19007  trcfilu  19867  cfilucfilOLD  20142  cfilucfil  20143  restmetu  20160  metucnOLD  20161  metucn  20162  cnheibor  20525  dvlip2  21465  tgifscgr  22959  tgcgrxfr  22968  tgbtwnconn1lem3  23004  tgbtwnconn1  23005  legtrd  23018  legtri3  23019  tglndim0  23033  tglinethru  23040  tglnpt2  23044  colline  23050  perpneq  23103  isperp2  23104  footex  23107  f1otrg  23115  eupatrl  23587  omndmul2  26173  isarchi3  26202  archirngz  26204  esumcst  26512  oms0  26708  eulerpartlemgvv  26757  signsply0  26950  signstfvneq0  26971  lgamucov  27022  cvmlift3lem2  27207  mblfinlem3  28427  mblfinlem4  28428  itg2addnclem2  28441  itg2gt0cn  28444  ftc1cnnc  28463  ftc1anc  28472  nn0prpwlem  28514  sstotbnd2  28670  pell1234qrdich  29199  pell14qrdich  29207  pell1qrgap  29212  climrec  29773  climsuse  29778  3cyclfrgra  30604  2spot0  30654  numclwlk2lem2f1o  30695  mndpsuppss  30781  ply1mulgsumlem2  30842  mptcoe1matfsupp  30888  pmatcollpw1dst  30898  mp2pm2mplem4  30916  pmattomply1mhmlem0  30924  pmattomply1mhmlem1  30925  lcfl8  35144
  Copyright terms: Public domain W3C validator