Theorem 3adant3r 1182

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 1165	1 ⊢ ((𝜑 ∧ 𝜓 ∧ (𝜒 ∧ 𝜏)) → 𝜃)

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

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 1088

This theorem is referenced by:  mapfien2  9288  cfeq0  10142  ltmul2  11967  lemul1  11968  lemul2  11969  lemuldiv  11997  lediv2  12007  ltdiv23  12008  lediv23  12009  dvdscmulr  16190  dvdsmulcr  16191  modremain  16314  ndvdsadd  16316  rpexp12i  16630  isdrngd  20675  isdrngdOLD  20677  cramerimp  22596  tsmsxp  24065  xblcntrps  24320  xblcntr  24321  rrxmet  25330  nvaddsub4  30629  hvmulcan2  31045  adjlnop  32058  rrnmet  37869  lfladd  39105  lflsub  39106  lshpset2N  39158  atcvrj1  39470  athgt  39495  ltrncnvel  40181  trlcnv  40204  trljat2  40206  cdlemc5  40234  trlcoabs  40760  trlcolem  40765  dicvaddcl  41229  limsupre3uzlem  45773  fourierdlem42  46187  ovnhoilem2  46640  lincext3  48488