Theorem ad4antr 764

Description: Deduction adding 4 conjuncts to antecedent. (Contributed by Mario Carneiro, 4-Jan-2017.)

Hypothesis

Ref	Expression
ad2ant.1	⊢ (𝜑 → 𝜓)

Assertion

Ref	Expression
ad4antr	⊢ (((((𝜑 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) → 𝜓)

Proof of Theorem ad4antr

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

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 196  df-an 385

This theorem is referenced by:  ad5antr  766  tfrlem1  7359  prdsval  15938  catass  16170  catpropd  16192  cidpropd  16193  subccocl  16328  funcco  16354  natpropd  16459  fucpropd  16460  initoeu2lem1  16487  prfval  16662  xpcpropd  16671  acsfiindd  17000  mhmmnd  17360  scmatscm  20138  cpmatmcllem  20342  mptcoe1matfsupp  20426  mp2pm2mplem4  20433  chpdmatlem2  20463  chfacfisf  20478  chfacfisfcpmat  20479  neitr  20794  hauscmplem  21019  trcfilu  21908  cfilucfil  22174  restmetu  22185  metucn  22186  cnheibor  22562  dvlip2  23562  lgamucov  24564  tgifscgr  25203  iscgrglt  25209  tgbtwnconn1  25270  legtrd  25284  legtri3  25285  legso  25294  hlcgrex  25311  tglndim0  25324  tglinethru  25331  tglnpt2  25336  colline  25344  perpneq  25409  isperp2  25410  footex  25413  opphllem  25427  midex  25429  opphllem3  25441  opphllem5  25443  opphllem6  25444  opphl  25446  outpasch  25447  hlpasch  25448  lnopp2hpgb  25455  hpgerlem  25457  lmieu  25476  trgcopy  25496  cgrahl  25518  acopy  25524  inaghl  25531  cgrg3col4  25534  f1otrg  25551  eupatrl  26495  3cyclfrgra  26542  2spot0  26591  numclwlk2lem2f1o  26632  omndmul2  29043  isarchi3  29072  archirngz  29074  psgnfzto1stlem  29181  qtophaus  29231  esumcst  29452  sigapildsys  29552  oms0  29686  omssubadd  29689  carsgclctunlem3  29709  eulerpartlemgvv  29765  signsply0  29954  signstfvneq0  29975  cvmlift3lem2  30556  nn0prpwlem  31487  lindsenlbs  32574  matunitlindflem1  32575  mblfinlem3  32618  mblfinlem4  32619  itg2addnclem2  32632  itg2gt0cn  32635  ftc1cnnc  32654  ftc1anc  32663  sstotbnd2  32743  lcfl8  35809  pell1234qrdich  36443  pell14qrdich  36451  pell1qrgap  36456  pellfundex  36468  cvgdvgrat  37534  infleinflem2  38528  xrralrecnnle  38543  climrec  38670  climsuse  38675  limcrecl  38696  fperdvper  38808  dvnprodlem2  38837  etransclem35  39162  hspmbllem2  39517  smflimlem2  39658  smflimlem4  39660  iccpartgt  39965  sfprmdvdsmersenne  40058  nbumgrvtx  40568  3cyclfrgr  41458  av-numclwlk2lem2f1o  41535  2zlidl  41724  mndpsuppss  41946  ply1mulgsumlem2  41969  nn0sumshdiglemA  42211