Theorem ad4antr 728

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

Syntax hints:   → wi 4   ∧ wa 395

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 396

This theorem is referenced by:  ad5antr  730  ad5antlr  731  simp-4l  779  tfrlem1  8178  prdsval  17083  catass  17312  catpropd  17335  cidpropd  17336  subccocl  17476  funcco  17502  natpropd  17610  fucpropd  17611  initoeu2lem1  17645  prfval  17832  xpcpropd  17842  acsfiindd  18186  mhmmnd  18612  mhpmulcl  21249  scmatscm  21570  cpmatmcllem  21775  mptcoe1matfsupp  21859  mp2pm2mplem4  21866  chpdmatlem2  21896  chfacfisf  21911  chfacfisfcpmat  21912  neitr  22239  hauscmplem  22465  trcfilu  23354  cfilucfil  23621  restmetu  23632  metucn  23633  cnheibor  24024  dvlip2  25064  lgamucov  26092  tgifscgr  26773  iscgrglt  26779  tgbtwnconn1  26840  legtrd  26854  legtri3  26855  legso  26864  hlcgrex  26881  tglndim0  26894  tglinethru  26901  tglnpt2  26906  colline  26914  perpneq  26979  isperp2  26980  footexALT  26983  opphllem  27000  midex  27002  opphllem3  27014  opphllem5  27016  opphllem6  27017  opphl  27019  outpasch  27020  hlpasch  27021  lnopp2hpgb  27028  hpgerlem  27030  lmieu  27049  lnperpex  27068  trgcopy  27069  cgrahl  27092  acopy  27098  inaghl  27110  cgrg3col4  27118  f1otrg  27136  nbumgrvtx  27616  3cyclfrgr  28553  numclwlk2lem2f1o  28644  s3f1  31123  dfmgc2  31176  pwrssmgc  31180  mgcf1o  31183  omndmul2  31240  psgnfzto1stlem  31269  cycpmrn  31312  tocyccntz  31313  cycpmconjs  31325  isarchi3  31343  archirngz  31345  nsgqusf1olem1  31500  nsgqusf1olem2  31501  nsgqusf1olem3  31502  rhmpreimaidl  31505  elrspunidl  31508  idlinsubrg  31510  rhmimaidl  31511  isprmidlc  31525  qsidomlem1  31530  qsidomlem2  31531  mxidlprm  31542  dimkerim  31610  fedgmul  31614  extdg1id  31640  qtophaus  31688  zarclsint  31724  zarcmplem  31733  esumcst  31931  sigapildsys  32030  oms0  32164  omssubadd  32167  carsgclctunlem3  32187  eulerpartlemgvv  32243  signsply0  32430  signstfvneq0  32451  actfunsnf1o  32484  reprsuc  32495  reprinfz1  32502  breprexplema  32510  breprexplemc  32512  hgt750lemb  32536  cvmlift3lem2  33182  satfdmlem  33230  nn0prpwlem  34438  lindsenlbs  35699  matunitlindflem1  35700  mblfinlem3  35743  mblfinlem4  35744  itg2addnclem2  35756  itg2gt0cn  35759  ftc1cnnc  35776  ftc1anc  35785  sstotbnd2  35859  lcfl8  39443  aks4d1p8  40023  fsuppind  40202  prjspersym  40367  pell1234qrdich  40599  pell14qrdich  40607  pell1qrgap  40612  pellfundex  40624  cvgdvgrat  41820  infleinflem2  42800  xrralrecnnle  42812  climrec  43034  climsuse  43039  limcrecl  43060  limsupubuz  43144  limsupgtlem  43208  xlimliminflimsup  43293  fperdvper  43350  dvnprodlem2  43378  etransclem35  43700  hspmbllem2  44055  smflimlem2  44194  smflimlem4  44196  iccpartgt  44767  prproropf1olem4  44846  sfprmdvdsmersenne  44943  isomushgr  45166  isomuspgrlem1  45167  isomuspgrlem2d  45171  2zlidl  45380  mndpsuppss  45595  ply1mulgsumlem2  45616  nn0sumshdiglemA  45853  functhinclem4  46213