Theorem ad4ant13 1292

Description: Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.)

Hypothesis

Ref	Expression
ad4ant13.1	⊢ ((𝜑 ∧ 𝜓) → 𝜒)

Assertion

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

Proof of Theorem ad4ant13

Step	Hyp	Ref	Expression
1		ad4ant13.1	. . . . 5 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
2	1	ex 450	. . . 4 ⊢ (𝜑 → (𝜓 → 𝜒))
3	2	a1dd 50	. . 3 ⊢ (𝜑 → (𝜓 → (𝜏 → 𝜒)))
4	3	a1d 25	. 2 ⊢ (𝜑 → (𝜃 → (𝜓 → (𝜏 → 𝜒))))
5	4	imp41 619	1 ⊢ ((((𝜑 ∧ 𝜃) ∧ 𝜓) ∧ 𝜏) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 384

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 386

This theorem is referenced by:  fntpb  6473  dvdslcmf  15344  poslubmo  17146  posglbmo  17147  trust  22033  metust  22363  umgrres1lem  26202  upgrres1  26205  friendshipgt3  27256  repr0  30689  breprexplemc  30710  hgt750lemb  30734  matunitlindflem1  33405  mapss2  39397  supxrge  39554  xrlexaddrp  39568  infxr  39583  infleinf  39588  unb2ltle  39642  supminfxr  39694  limsuppnfdlem  39933  limsupub  39936  limsuppnflem  39942  climinf3  39948  limsupmnflem  39952  climxrre  39982  liminfvalxr  40015  sge0isum  40644  sge0gtfsumgt  40660  sge0seq  40663  nnfoctbdjlem  40672  omeiunltfirp  40733  hspdifhsp  40830  hspmbllem2  40841  pimdecfgtioo  40927  pimincfltioo  40928  preimageiingt  40930  preimaleiinlt  40931  smfid  40961  proththd  41531