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

Theorem ad4antr 763
Description: Deduction adding 4 conjuncts to antecedent. (Contributed by Mario Carneiro, 4-Jan-2017.)
Hypothesis
Ref Expression
ad2ant.1 (𝜑𝜓)
Assertion
Ref Expression
ad4antr (((((𝜑𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) → 𝜓)

Proof of Theorem ad4antr
StepHypRef Expression
1 ad2ant.1 . . 3 (𝜑𝜓)
21ad3antrrr 761 . 2 ((((𝜑𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜓)
32adantr 479 1 (((((𝜑𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382
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 195  df-an 384
This theorem is referenced by:  ad5antr  765  tfrlem1  7336  prdsval  15884  catass  16116  catpropd  16138  cidpropd  16139  subccocl  16274  funcco  16300  natpropd  16405  fucpropd  16406  initoeu2lem1  16433  prfval  16608  xpcpropd  16617  acsfiindd  16946  mhmmnd  17306  scmatscm  20080  cpmatmcllem  20284  mptcoe1matfsupp  20368  mp2pm2mplem4  20375  chpdmatlem2  20405  chfacfisf  20420  chfacfisfcpmat  20421  neitr  20736  hauscmplem  20961  trcfilu  21850  cfilucfil  22115  restmetu  22126  metucn  22127  cnheibor  22493  dvlip2  23479  lgamucov  24481  tgifscgr  25121  iscgrglt  25127  tgbtwnconn1  25188  legtrd  25202  legtri3  25203  legso  25212  hlcgrex  25229  tglndim0  25242  tglinethru  25249  tglnpt2  25254  colline  25262  perpneq  25327  isperp2  25328  footex  25331  opphllem  25345  midex  25347  opphllem3  25359  opphllem5  25361  opphllem6  25362  opphl  25364  outpasch  25365  hlpasch  25366  lnopp2hpgb  25373  hpgerlem  25375  lmieu  25394  trgcopy  25414  cgrahl  25436  acopy  25442  inaghl  25449  cgrg3col4  25452  f1otrg  25469  eupatrl  26261  3cyclfrgra  26308  2spot0  26357  numclwlk2lem2f1o  26398  omndmul2  28849  isarchi3  28878  archirngz  28880  psgnfzto1stlem  28987  qtophaus  29037  esumcst  29258  sigapildsys  29358  oms0  29492  omssubadd  29495  carsgclctunlem3  29515  eulerpartlemgvv  29571  signsply0  29760  signstfvneq0  29781  cvmlift3lem2  30362  nn0prpwlem  31293  lindsenlbs  32370  matunitlindflem1  32371  mblfinlem3  32414  mblfinlem4  32415  itg2addnclem2  32428  itg2gt0cn  32431  ftc1cnnc  32450  ftc1anc  32459  sstotbnd2  32539  lcfl8  35605  pell1234qrdich  36239  pell14qrdich  36247  pell1qrgap  36252  pellfundex  36264  cvgdvgrat  37330  infleinflem2  38325  xrralrecnnle  38340  climrec  38467  climsuse  38472  limcrecl  38493  fperdvper  38605  dvnprodlem2  38634  etransclem35  38959  hspmbllem2  39314  smflimlem2  39455  smflimlem4  39457  iccpartgt  39763  sfprmdvdsmersenne  39856  nbumgrvtx  40563  3cyclfrgr  41453  av-numclwlk2lem2f1o  41530  2zlidl  41719  mndpsuppss  41941  ply1mulgsumlem2  41964  nn0sumshdiglemA  42206
  Copyright terms: Public domain W3C validator