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 482 . 2 ((𝜑𝜒) → 𝜓)
32ad3antrrr 729 1 (((((𝜑𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397
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 206  df-an 398
This theorem is referenced by:  ad5antr  733  ad5antlr  734  simp-4l  782  tfrlem1  8323  prdsval  17338  catass  17567  catpropd  17590  cidpropd  17591  subccocl  17732  funcco  17758  natpropd  17866  fucpropd  17867  initoeu2lem1  17901  prfval  18088  xpcpropd  18098  acsfiindd  18443  mhmmnd  18870  mhpmulcl  21542  scmatscm  21865  cpmatmcllem  22070  mptcoe1matfsupp  22154  mp2pm2mplem4  22161  chpdmatlem2  22191  chfacfisf  22206  chfacfisfcpmat  22207  neitr  22534  hauscmplem  22760  trcfilu  23649  cfilucfil  23918  restmetu  23929  metucn  23930  cnheibor  24321  dvlip2  25362  lgamucov  26390  tgifscgr  27453  iscgrglt  27459  tgbtwnconn1  27520  legtrd  27534  legtri3  27535  legso  27544  hlcgrex  27561  tglndim0  27574  tglinethru  27581  tglnpt2  27586  colline  27594  perpneq  27659  isperp2  27660  footexALT  27663  opphllem  27680  midex  27682  opphllem3  27694  opphllem5  27696  opphllem6  27697  opphl  27699  outpasch  27700  hlpasch  27701  lnopp2hpgb  27708  hpgerlem  27710  lmieu  27729  lnperpex  27748  trgcopy  27749  cgrahl  27772  acopy  27778  inaghl  27790  cgrg3col4  27798  f1otrg  27816  nbumgrvtx  28297  3cyclfrgr  29235  numclwlk2lem2f1o  29326  s3f1  31806  dfmgc2  31859  pwrssmgc  31863  mgcf1o  31866  omndmul2  31923  psgnfzto1stlem  31952  cycpmrn  31995  tocyccntz  31996  cycpmconjs  32008  isarchi3  32026  archirngz  32028  nsgqusf1olem1  32194  nsgqusf1olem2  32195  nsgqusf1olem3  32196  ghmqusker  32201  rhmpreimaidl  32203  elrspunidl  32206  idlinsubrg  32208  rhmimaidl  32209  isprmidlc  32223  qsidomlem1  32228  qsidomlem2  32229  mxidlprm  32240  dimkerim  32325  fedgmul  32329  extdg1id  32355  qtophaus  32420  zarclsint  32456  zarcmplem  32465  esumcst  32665  sigapildsys  32764  oms0  32900  omssubadd  32903  carsgclctunlem3  32923  eulerpartlemgvv  32979  signsply0  33166  signstfvneq0  33187  actfunsnf1o  33220  reprsuc  33231  reprinfz1  33238  breprexplema  33246  breprexplemc  33248  hgt750lemb  33272  cvmlift3lem2  33917  satfdmlem  33965  nn0prpwlem  34797  lindsenlbs  36076  matunitlindflem1  36077  mblfinlem3  36120  mblfinlem4  36121  itg2addnclem2  36133  itg2gt0cn  36136  ftc1cnnc  36153  ftc1anc  36162  sstotbnd2  36236  lcfl8  39968  aks4d1p8  40547  fldhmf1  40550  aks6d1c2p2  40552  fsuppind  40768  prjspersym  40948  pell1234qrdich  41187  pell14qrdich  41195  pell1qrgap  41200  pellfundex  41212  omabs2  41668  cvgdvgrat  42600  infleinflem2  43612  xrralrecnnle  43624  climrec  43851  climsuse  43856  limcrecl  43877  limsupubuz  43961  limsupgtlem  44025  xlimliminflimsup  44110  fperdvper  44167  dvnprodlem2  44195  etransclem35  44517  hspmbllem2  44875  smflimlem2  45020  smflimlem4  45022  iccpartgt  45626  prproropf1olem4  45705  sfprmdvdsmersenne  45802  isomushgr  46025  isomuspgrlem1  46026  isomuspgrlem2d  46030  2zlidl  46239  mndpsuppss  46454  ply1mulgsumlem2  46475  nn0sumshdiglemA  46712  functhinclem4  47071
  Copyright terms: Public domain W3C validator