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

Theorem ad4antr 729
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 727 . 2  |-  ( ( ( ( ph  /\  ch )  /\  th )  /\  ta )  ->  ps )
32adantr 463 1  |-  ( ( ( ( ( ph  /\ 
ch )  /\  th )  /\  ta )  /\  et )  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367
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 369
This theorem is referenced by:  ad5antr  731  tfrlem1  7037  prdsval  14947  catass  15178  catpropd  15200  cidpropd  15201  subccocl  15336  funcco  15362  natpropd  15467  fucpropd  15468  initoeu2lem1  15495  prfval  15670  xpcpropd  15679  acsfiindd  16009  mhmmnd  16394  scmatscm  19185  cpmatmcllem  19389  mptcoe1matfsupp  19473  mp2pm2mplem4  19480  chpdmatlem2  19510  chfacfisf  19525  chfacfisfcpmat  19526  neitr  19851  hauscmplem  20076  trcfilu  20966  cfilucfilOLD  21241  cfilucfil  21242  restmetu  21259  metucnOLD  21260  metucn  21261  cnheibor  21624  dvlip2  22565  tgifscgr  24104  tgbtwnconn1  24166  legtrd  24180  legtri3  24181  legso  24189  tglndim0  24213  tglinethru  24220  tglnpt2  24225  colline  24234  perpneq  24295  isperp2  24296  footex  24299  opphllem  24313  midex  24315  opphllem3  24325  opphllem5  24327  opphllem6  24328  opphl  24329  lnopp2hpgb  24336  hpgerlem  24338  lmieu  24354  f1otrg  24379  eupatrl  25173  3cyclfrgra  25220  2spot0  25269  numclwlk2lem2f1o  25310  omndmul2  27939  isarchi3  27968  archirngz  27970  qtophaus  28077  esumcst  28295  sigapildsys  28391  oms0  28508  omssubadd  28511  carsgclctunlem3  28531  eulerpartlemgvv  28582  signsply0  28775  signstfvneq0  28796  lgamucov  28847  cvmlift3lem2  29032  mblfinlem3  30296  mblfinlem4  30297  itg2addnclem2  30310  itg2gt0cn  30313  ftc1cnnc  30332  ftc1anc  30341  nn0prpwlem  30383  sstotbnd2  30513  pell1234qrdich  31039  pell14qrdich  31047  pell1qrgap  31052  pellfundex  31064  cvgdvgrat  31438  climrec  31851  climsuse  31856  limcrecl  31877  fperdvper  31957  dvnprodlem2  31986  etransclem35  32294  2zlidl  33013  mndpsuppss  33237  ply1mulgsumlem2  33260  nn0sumshdiglemA  33513  lcfl8  37645
  Copyright terms: Public domain W3C validator