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

Theorem ad4antr 731
Description: Deduction adding 4 conjuncts to antecedent. (Contributed by Mario Carneiro, 4-Jan-2017.) (Proof shortened by Wolf Lammen, 5-Apr-2022.)
Hypothesis
Ref Expression
ad2ant.1 (𝜑𝜓)
Assertion
Ref Expression
ad4antr (((((𝜑𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) → 𝜓)

Proof of Theorem ad4antr
StepHypRef Expression
1 ad2ant.1 . . 3 (𝜑𝜓)
21adantr 484 . 2 ((𝜑𝜒) → 𝜓)
32ad3antrrr 729 1 (((((𝜑𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399
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 210  df-an 400
This theorem is referenced by:  ad5antr  733  ad5antlr  734  simp-4l  782  tfrlem1  7999  prdsval  16724  catass  16953  catpropd  16975  cidpropd  16976  subccocl  17111  funcco  17137  natpropd  17242  fucpropd  17243  initoeu2lem1  17270  prfval  17445  xpcpropd  17454  acsfiindd  17783  mhmmnd  18217  scmatscm  21122  cpmatmcllem  21327  mptcoe1matfsupp  21411  mp2pm2mplem4  21418  chpdmatlem2  21448  chfacfisf  21463  chfacfisfcpmat  21464  neitr  21789  hauscmplem  22015  trcfilu  22904  cfilucfil  23170  restmetu  23181  metucn  23182  cnheibor  23564  dvlip2  24602  lgamucov  25627  tgifscgr  26306  iscgrglt  26312  tgbtwnconn1  26373  legtrd  26387  legtri3  26388  legso  26397  hlcgrex  26414  tglndim0  26427  tglinethru  26434  tglnpt2  26439  colline  26447  perpneq  26512  isperp2  26513  footexALT  26516  opphllem  26533  midex  26535  opphllem3  26547  opphllem5  26549  opphllem6  26550  opphl  26552  outpasch  26553  hlpasch  26554  lnopp2hpgb  26561  hpgerlem  26563  lmieu  26582  lnperpex  26601  trgcopy  26602  cgrahl  26625  acopy  26631  inaghl  26643  cgrg3col4  26651  f1otrg  26669  nbumgrvtx  27140  3cyclfrgr  28077  numclwlk2lem2f1o  28168  s3f1  30653  dfmgc2  30708  pwrssmgc  30710  omndmul2  30767  psgnfzto1stlem  30796  cycpmrn  30839  tocyccntz  30840  cycpmconjs  30852  isarchi3  30870  archirngz  30872  rhmpreimaidl  31015  elrspunidl  31018  idlinsubrg  31020  rhmimaidl  31021  isprmidlc  31035  qsidomlem1  31040  qsidomlem2  31041  mxidlprm  31052  dimkerim  31115  fedgmul  31119  extdg1id  31145  qtophaus  31193  zarclsint  31229  zarcmplem  31238  esumcst  31436  sigapildsys  31535  oms0  31669  omssubadd  31672  carsgclctunlem3  31692  eulerpartlemgvv  31748  signsply0  31935  signstfvneq0  31956  actfunsnf1o  31989  reprsuc  32000  reprinfz1  32007  breprexplema  32015  breprexplemc  32017  hgt750lemb  32041  cvmlift3lem2  32681  satfdmlem  32729  nn0prpwlem  33784  lindsenlbs  35051  matunitlindflem1  35052  mblfinlem3  35095  mblfinlem4  35096  itg2addnclem2  35108  itg2gt0cn  35111  ftc1cnnc  35128  ftc1anc  35137  sstotbnd2  35211  lcfl8  38797  fsuppind  39453  prjspersym  39598  pell1234qrdich  39799  pell14qrdich  39807  pell1qrgap  39812  pellfundex  39824  cvgdvgrat  41014  infleinflem2  42000  xrralrecnnle  42014  climrec  42242  climsuse  42247  limcrecl  42268  limsupubuz  42352  limsupgtlem  42416  xlimliminflimsup  42501  fperdvper  42558  dvnprodlem2  42586  etransclem35  42908  hspmbllem2  43263  smflimlem2  43402  smflimlem4  43404  iccpartgt  43941  prproropf1olem4  44020  sfprmdvdsmersenne  44118  isomushgr  44341  isomuspgrlem1  44342  isomuspgrlem2d  44346  2zlidl  44555  mndpsuppss  44770  ply1mulgsumlem2  44792  nn0sumshdiglemA  45030
  Copyright terms: Public domain W3C validator