Theorem 3adant3r 1189

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

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

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

This theorem is referenced by:  mapfien2  9316  cfeq0  10173  ltmul2  12001  lemul1  12002  lemul2  12003  lemuldiv  12031  lediv2  12041  ltdiv23  12042  lediv23  12043  dvdscmulr  16248  dvdsmulcr  16249  modremain  16372  ndvdsadd  16374  rpexp12i  16689  isdrngd  20741  isdrngdOLD  20743  cramerimp  22673  tsmsxp  24142  xblcntrps  24397  xblcntr  24398  rrxmet  25397  nvaddsub4  30750  hvmulcan2  31166  adjlnop  32179  rrnmet  38211  lfladd  39573  lflsub  39574  lshpset2N  39626  atcvrj1  39938  athgt  39963  ltrncnvel  40649  trlcnv  40672  trljat2  40674  cdlemc5  40702  trlcoabs  41228  trlcolem  41233  dicvaddcl  41697  limsupre3uzlem  46192  fourierdlem42  46606  ovnhoilem2  47059  lincext3  48961