Theorem 3adant3r 1181

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ 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 206  df-an 397  df-3an 1089

This theorem is referenced by:  wfrlem12OLD  8316  mapfien2  9400  cfeq0  10247  ltmul2  12061  lemul1  12062  lemul2  12063  lemuldiv  12090  lediv2  12100  ltdiv23  12101  lediv23  12102  dvdscmulr  16224  dvdsmulcr  16225  modremain  16347  ndvdsadd  16349  rpexp12i  16657  isdrngd  20340  isdrngdOLD  20342  cramerimp  22179  tsmsxp  23650  xblcntrps  23907  xblcntr  23908  rrxmet  24916  nvaddsub4  29897  hvmulcan2  30313  adjlnop  31326  rrnmet  36685  lfladd  37924  lflsub  37925  lshpset2N  37977  atcvrj1  38290  athgt  38315  ltrncnvel  39001  trlcnv  39024  trljat2  39026  cdlemc5  39054  trlcoabs  39580  trlcolem  39585  dicvaddcl  40049  limsupre3uzlem  44437  fourierdlem42  44851  ovnhoilem2  45304  lincext3  47090