Theorem 3adant3r 1183

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 482	. 2 ⊢ ((𝜒 ∧ 𝜏) → 𝜒)
2		ad4ant3.1	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
3	1, 2	syl3an3 1166	1 ⊢ ((𝜑 ∧ 𝜓 ∧ (𝜒 ∧ 𝜏)) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087

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 207  df-an 396  df-3an 1089

This theorem is referenced by:  mapfien2  9324  cfeq0  10178  ltmul2  12004  lemul1  12005  lemul2  12006  lemuldiv  12034  lediv2  12044  ltdiv23  12045  lediv23  12046  dvdscmulr  16223  dvdsmulcr  16224  modremain  16347  ndvdsadd  16349  rpexp12i  16663  isdrngd  20710  isdrngdOLD  20712  cramerimp  22642  tsmsxp  24111  xblcntrps  24366  xblcntr  24367  rrxmet  25376  nvaddsub4  30744  hvmulcan2  31160  adjlnop  32173  rrnmet  38077  lfladd  39439  lflsub  39440  lshpset2N  39492  atcvrj1  39804  athgt  39829  ltrncnvel  40515  trlcnv  40538  trljat2  40540  cdlemc5  40568  trlcoabs  41094  trlcolem  41099  dicvaddcl  41563  limsupre3uzlem  46090  fourierdlem42  46504  ovnhoilem2  46957  lincext3  48813