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

Theorem ad4antr 769
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 480 . 2 ((𝜑𝜒) → 𝜓)
32ad3antrrr 766 1 (((((𝜑𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383
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 197  df-an 385
This theorem is referenced by:  ad5antr  773  ad5antrOLD  774  ad5antlr  775  tfrlem1  7517  prdsval  16162  catass  16394  catpropd  16416  cidpropd  16417  subccocl  16552  funcco  16578  natpropd  16683  fucpropd  16684  initoeu2lem1  16711  prfval  16886  xpcpropd  16895  acsfiindd  17224  mhmmnd  17584  scmatscm  20367  cpmatmcllem  20571  mptcoe1matfsupp  20655  mp2pm2mplem4  20662  chpdmatlem2  20692  chfacfisf  20707  chfacfisfcpmat  20708  neitr  21032  hauscmplem  21257  trcfilu  22145  cfilucfil  22411  restmetu  22422  metucn  22423  cnheibor  22801  dvlip2  23803  lgamucov  24809  tgifscgr  25448  iscgrglt  25454  tgbtwnconn1  25515  legtrd  25529  legtri3  25530  legso  25539  hlcgrex  25556  tglndim0  25569  tglinethru  25576  tglnpt2  25581  colline  25589  perpneq  25654  isperp2  25655  footex  25658  opphllem  25672  midex  25674  opphllem3  25686  opphllem5  25688  opphllem6  25689  opphl  25691  outpasch  25692  hlpasch  25693  lnopp2hpgb  25700  hpgerlem  25702  lmieu  25721  trgcopy  25741  cgrahl  25763  acopy  25769  inaghl  25776  cgrg3col4  25779  f1otrg  25796  nbumgrvtx  26287  3cyclfrgr  27268  numclwlk2lem2f1o  27359  numclwlk2lem2f1oOLD  27366  omndmul2  29840  isarchi3  29869  archirngz  29871  psgnfzto1stlem  29978  qtophaus  30031  esumcst  30253  sigapildsys  30353  oms0  30487  omssubadd  30490  carsgclctunlem3  30510  eulerpartlemgvv  30566  signsply0  30756  signstfvneq0  30777  actfunsnf1o  30810  reprsuc  30821  reprinfz1  30828  breprexplema  30836  breprexplemc  30838  hgt750lemb  30862  cvmlift3lem2  31428  nn0prpwlem  32442  lindsenlbs  33534  matunitlindflem1  33535  mblfinlem3  33578  mblfinlem4  33579  itg2addnclem2  33592  itg2gt0cn  33595  ftc1cnnc  33614  ftc1anc  33623  sstotbnd2  33703  lcfl8  37108  pell1234qrdich  37742  pell14qrdich  37750  pell1qrgap  37755  pellfundex  37767  cvgdvgrat  38829  infleinflem2  39900  xrralrecnnle  39915  climrec  40153  climsuse  40158  limcrecl  40179  limsupubuz  40263  limsupgtlem  40327  fperdvper  40451  dvnprodlem2  40480  etransclem35  40804  hspmbllem2  41162  smflimlem2  41301  smflimlem4  41303  iccpartgt  41688  sfprmdvdsmersenne  41845  2zlidl  42259  mndpsuppss  42477  ply1mulgsumlem2  42500  nn0sumshdiglemA  42738
  Copyright terms: Public domain W3C validator