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

Syntax hints:   → wi 4   ∧ wa 397   ∧ w3a 1088

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 398  df-3an 1090

This theorem is referenced by:  wfrlem12OLD  8320  mapfien2  9404  cfeq0  10251  ltmul2  12065  lemul1  12066  lemul2  12067  lemuldiv  12094  lediv2  12104  ltdiv23  12105  lediv23  12106  dvdscmulr  16228  dvdsmulcr  16229  modremain  16351  ndvdsadd  16353  rpexp12i  16661  isdrngd  20390  isdrngdOLD  20392  cramerimp  22188  tsmsxp  23659  xblcntrps  23916  xblcntr  23917  rrxmet  24925  nvaddsub4  29910  hvmulcan2  30326  adjlnop  31339  rrnmet  36697  lfladd  37936  lflsub  37937  lshpset2N  37989  atcvrj1  38302  athgt  38327  ltrncnvel  39013  trlcnv  39036  trljat2  39038  cdlemc5  39066  trlcoabs  39592  trlcolem  39597  dicvaddcl  40061  limsupre3uzlem  44451  fourierdlem42  44865  ovnhoilem2  45318  lincext3  47137