Theorem ad4antr 730

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 483	. 2 ⊢ ((𝜑 ∧ 𝜒) → 𝜓)
3	2	ad3antrrr 728	1 ⊢ (((((𝜑 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  ad5antr  732  ad5antlr  733  simp-4l  781  tfrlem1  8012  prdsval  16728  catass  16957  catpropd  16979  cidpropd  16980  subccocl  17115  funcco  17141  natpropd  17246  fucpropd  17247  initoeu2lem1  17274  prfval  17449  xpcpropd  17458  acsfiindd  17787  mhmmnd  18221  scmatscm  21122  cpmatmcllem  21326  mptcoe1matfsupp  21410  mp2pm2mplem4  21417  chpdmatlem2  21447  chfacfisf  21462  chfacfisfcpmat  21463  neitr  21788  hauscmplem  22014  trcfilu  22903  cfilucfil  23169  restmetu  23180  metucn  23181  cnheibor  23559  dvlip2  24592  lgamucov  25615  tgifscgr  26294  iscgrglt  26300  tgbtwnconn1  26361  legtrd  26375  legtri3  26376  legso  26385  hlcgrex  26402  tglndim0  26415  tglinethru  26422  tglnpt2  26427  colline  26435  perpneq  26500  isperp2  26501  footexALT  26504  opphllem  26521  midex  26523  opphllem3  26535  opphllem5  26537  opphllem6  26538  opphl  26540  outpasch  26541  hlpasch  26542  lnopp2hpgb  26549  hpgerlem  26551  lmieu  26570  lnperpex  26589  trgcopy  26590  cgrahl  26613  acopy  26619  inaghl  26631  cgrg3col4  26639  f1otrg  26657  nbumgrvtx  27128  3cyclfrgr  28067  numclwlk2lem2f1o  28158  s3f1  30623  omndmul2  30713  psgnfzto1stlem  30742  cycpmrn  30785  tocyccntz  30786  cycpmconjs  30798  isarchi3  30816  archirngz  30818  isprmidlc  30963  qsidomlem1  30965  qsidomlem2  30966  mxidlprm  30977  dimkerim  31023  fedgmul  31027  extdg1id  31053  qtophaus  31100  esumcst  31322  sigapildsys  31421  oms0  31555  omssubadd  31558  carsgclctunlem3  31578  eulerpartlemgvv  31634  signsply0  31821  signstfvneq0  31842  actfunsnf1o  31875  reprsuc  31886  reprinfz1  31893  breprexplema  31901  breprexplemc  31903  hgt750lemb  31927  cvmlift3lem2  32567  satfdmlem  32615  nn0prpwlem  33670  lindsenlbs  34902  matunitlindflem1  34903  mblfinlem3  34946  mblfinlem4  34947  itg2addnclem2  34959  itg2gt0cn  34962  ftc1cnnc  34981  ftc1anc  34990  sstotbnd2  35067  lcfl8  38653  prjspersym  39277  pell1234qrdich  39478  pell14qrdich  39486  pell1qrgap  39491  pellfundex  39503  cvgdvgrat  40665  infleinflem2  41659  xrralrecnnle  41673  climrec  41904  climsuse  41909  limcrecl  41930  limsupubuz  42014  limsupgtlem  42078  xlimliminflimsup  42163  fperdvper  42223  dvnprodlem2  42252  etransclem35  42574  hspmbllem2  42929  smflimlem2  43068  smflimlem4  43070  iccpartgt  43607  prproropf1olem4  43688  sfprmdvdsmersenne  43788  isomushgr  44011  isomuspgrlem1  44012  isomuspgrlem2d  44016  2zlidl  44225  mndpsuppss  44439  ply1mulgsumlem2  44461  nn0sumshdiglemA  44699