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

Theorem ad4antr 743
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 741 . 2  |-  ( ( ( ( ph  /\  ch )  /\  th )  /\  ta )  ->  ps )
32adantr 471 1  |-  ( ( ( ( ( ph  /\ 
ch )  /\  th )  /\  ta )  /\  et )  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 375
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 190  df-an 377
This theorem is referenced by:  ad5antr  745  tfrlem1  7119  prdsval  15401  catass  15640  catpropd  15662  cidpropd  15663  subccocl  15798  funcco  15824  natpropd  15929  fucpropd  15930  initoeu2lem1  15957  prfval  16132  xpcpropd  16141  acsfiindd  16471  mhmmnd  16856  scmatscm  19586  cpmatmcllem  19790  mptcoe1matfsupp  19874  mp2pm2mplem4  19881  chpdmatlem2  19911  chfacfisf  19926  chfacfisfcpmat  19927  neitr  20244  hauscmplem  20469  trcfilu  21357  cfilucfil  21622  restmetu  21633  metucn  21634  cnheibor  22031  dvlip2  22995  lgamucov  24011  tgifscgr  24601  iscgrglt  24607  tgbtwnconn1  24668  legtrd  24682  legtri3  24683  legso  24692  hlcgrex  24709  tglndim0  24722  tglinethru  24729  tglnpt2  24734  colline  24742  perpneq  24807  isperp2  24808  footex  24811  opphllem  24825  midex  24827  opphllem3  24839  opphllem5  24841  opphllem6  24842  opphl  24844  outpasch  24845  hlpasch  24846  lnopp2hpgb  24853  hpgerlem  24855  lmieu  24874  trgcopy  24894  cgrahl  24916  acopy  24922  inaghl  24929  cgrg3col4  24932  f1otrg  24949  eupatrl  25744  3cyclfrgra  25791  2spot0  25840  numclwlk2lem2f1o  25881  omndmul2  28523  isarchi3  28552  archirngz  28554  psgnfzto1stlem  28661  qtophaus  28711  esumcst  28932  sigapildsys  29032  oms0  29173  omssubadd  29176  oms0OLD  29177  omssubaddOLD  29180  carsgclctunlem3  29200  eulerpartlemgvv  29257  signsply0  29488  signstfvneq0  29509  cvmlift3lem2  30091  nn0prpwlem  31026  mblfinlem3  32023  mblfinlem4  32024  itg2addnclem2  32038  itg2gt0cn  32041  ftc1cnnc  32060  ftc1anc  32069  sstotbnd2  32150  lcfl8  35114  pell1234qrdich  35751  pell14qrdich  35759  pell1qrgap  35764  pellfundex  35778  cvgdvgrat  36705  climrec  37718  climsuse  37724  limcrecl  37746  fperdvper  37827  dvnprodlem2  37859  etransclem35  38171  hspmbllem2  38486  iccpartgt  38778  nbumgrvtx  39463  2zlidl  40206  mndpsuppss  40428  ply1mulgsumlem2  40451  nn0sumshdiglemA  40702
  Copyright terms: Public domain W3C validator