Theorem 3adant3r 1180

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

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

This theorem is referenced by:  wfrlem12OLD  8151  mapfien2  9168  cfeq0  10012  ltmul2  11826  lemul1  11827  lemul2  11828  lemuldiv  11855  lediv2  11865  ltdiv23  11866  lediv23  11867  dvdscmulr  15994  dvdsmulcr  15995  modremain  16117  ndvdsadd  16119  rpexp12i  16429  isdrngd  20016  cramerimp  21835  tsmsxp  23306  xblcntrps  23563  xblcntr  23564  rrxmet  24572  nvaddsub4  29019  hvmulcan2  29435  adjlnop  30448  rrnmet  35987  lfladd  37080  lflsub  37081  lshpset2N  37133  atcvrj1  37445  athgt  37470  ltrncnvel  38156  trlcnv  38179  trljat2  38181  cdlemc5  38209  trlcoabs  38735  trlcolem  38740  dicvaddcl  39204  limsupre3uzlem  43276  fourierdlem42  43690  ovnhoilem2  44140  lincext3  45797