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  9372  cfeq0  10251  ltmul2  12077  lemul1  12078  lemul2  12079  lemuldiv  12106  lediv2  12116  ltdiv23  12117  lediv23  12118  dvdscmulr  16359  dvdsmulcr  16360  modremain  16483  ndvdsadd  16485  rpexp12i  16800  isdrngd  20897  isdrngdOLD  20899  cramerimp  22872  tsmsxp  24341  xblcntrps  24596  xblcntr  24597  rrxmet  25596  nvaddsub4  31038  hvmulcan2  31454  adjlnop  32467  rrnmet  38513  lfladd  39873  lflsub  39874  lshpset2N  39926  atcvrj1  40238  athgt  40263  ltrncnvel  40949  trlcnv  40972  trljat2  40974  cdlemc5  41002  trlcoabs  41528  trlcolem  41533  dicvaddcl  41997  limsupre3uzlem  46482  fourierdlem42  46896  ovnhoilem2  47349  lincext3  49269