Theorem ad4antr 719

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

Step	Hyp	Ref	Expression
1		ad2ant.1	. . 3 ⊢ (𝜑 → 𝜓)
2	1	adantr 473	. 2 ⊢ ((𝜑 ∧ 𝜒) → 𝜓)
3	2	ad3antrrr 717	1 ⊢ (((((𝜑 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 387

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 199  df-an 388

This theorem is referenced by:  ad5antr  721  ad5antlr  722  simp-4l  770  simp-5r  773  tfrlem1  7816  prdsval  16584  catass  16815  catpropd  16837  cidpropd  16838  subccocl  16973  funcco  16999  natpropd  17104  fucpropd  17105  initoeu2lem1  17132  prfval  17307  xpcpropd  17316  acsfiindd  17645  mhmmnd  18008  scmatscm  20826  cpmatmcllem  21030  mptcoe1matfsupp  21114  mp2pm2mplem4  21121  chpdmatlem2  21151  chfacfisf  21166  chfacfisfcpmat  21167  neitr  21492  hauscmplem  21718  trcfilu  22606  cfilucfil  22872  restmetu  22883  metucn  22884  cnheibor  23262  dvlip2  24295  lgamucov  25317  tgifscgr  25996  iscgrglt  26002  tgbtwnconn1  26063  legtrd  26077  legtri3  26078  legso  26087  hlcgrex  26104  tglndim0  26117  tglinethru  26124  tglnpt2  26129  colline  26137  perpneq  26202  isperp2  26203  footexALT  26206  opphllem  26223  midex  26225  opphllem3  26237  opphllem5  26239  opphllem6  26240  opphl  26242  outpasch  26243  hlpasch  26244  lnopp2hpgb  26251  hpgerlem  26253  lmieu  26272  lnperpex  26291  trgcopy  26292  cgrahl  26315  acopy  26322  inaghl  26334  cgrg3col4  26342  f1otrg  26360  nbumgrvtx  26831  3cyclfrgr  27822  numclwlk2lem2f1o  27932  numclwlk2lem2f1oOLD  27935  s3f1  30372  omndmul2  30437  isarchi3  30488  archirngz  30490  dimkerim  30658  fedgmul  30662  extdg1id  30688  psgnfzto1stlem  30697  qtophaus  30750  esumcst  30972  sigapildsys  31072  oms0  31206  omssubadd  31209  carsgclctunlem3  31229  eulerpartlemgvv  31285  signsply0  31473  signstfvneq0  31495  actfunsnf1o  31529  reprsuc  31540  reprinfz1  31547  breprexplema  31555  breprexplemc  31557  hgt750lemb  31581  cvmlift3lem2  32158  nn0prpwlem  33197  lindsenlbs  34334  matunitlindflem1  34335  mblfinlem3  34378  mblfinlem4  34379  itg2addnclem2  34391  itg2gt0cn  34394  ftc1cnnc  34413  ftc1anc  34422  sstotbnd2  34500  lcfl8  38089  prjspersym  38670  pell1234qrdich  38860  pell14qrdich  38868  pell1qrgap  38873  pellfundex  38885  cvgdvgrat  40067  infleinflem2  41074  xrralrecnnle  41089  climrec  41321  climsuse  41326  limcrecl  41347  limsupubuz  41431  limsupgtlem  41495  xlimliminflimsup  41580  fperdvper  41639  dvnprodlem2  41668  etransclem35  41991  hspmbllem2  42346  smflimlem2  42485  smflimlem4  42487  iccpartgt  42965  prproropf1olem4  43042  sfprmdvdsmersenne  43142  isomushgr  43365  isomuspgrlem1  43366  isomuspgrlem2d  43370  2zlidl  43575  mndpsuppss  43791  ply1mulgsumlem2  43814  nn0sumshdiglemA  44053