Theorem 3adant3r 1200

Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 8-Jan-2006.) (Proof shortened by Wolf Lammen, 25-Jun-2022.)

Hypothesis

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

Assertion

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

Proof of Theorem 3adant3r

Step	Hyp	Ref	Expression
1		simpl 488	. 2 ⊢ ((𝜒 ∧ 𝜏) → 𝜒)
2		ad4ant3.1	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
3	1, 2	syl3an3 1183	1 ⊢ ((𝜑 ∧ 𝜓 ∧ (𝜒 ∧ 𝜏)) → 𝜃)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  mapfien2  9405  cfeq0  10338  ltmul2  12172  lemul1  12173  lemul2  12174  lemuldiv  12201  lediv2  12211  ltdiv23  12212  lediv23  12213  dvdscmulr  16460  dvdsmulcr  16461  modremain  16584  ndvdsadd  16586  rpexp12i  16906  isdrngd  21028  isdrngdOLD  21030  cramerimp  23010  tsmsxp  24480  xblcntrps  24735  xblcntr  24736  rrxmet  25735  nvaddsub4  31265  hvmulcan2  31681  adjlnop  32694  rrnmet  38857  lfladd  40217  lflsub  40218  lshpset2N  40270  atcvrj1  40582  athgt  40607  ltrncnvel  41293  trlcnv  41316  trljat2  41318  cdlemc5  41346  trlcoabs  41872  trlcolem  41877  dicvaddcl  42341  limsupre3uzlem  46839  fourierdlem42  47253  ovnhoilem2  47706  lincext3  49662