Theorem 3adant3r 1200

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  mapfien2  9394  cfeq0  10327  ltmul2  12161  lemul1  12162  lemul2  12163  lemuldiv  12190  lediv2  12200  ltdiv23  12201  lediv23  12202  dvdscmulr  16447  dvdsmulcr  16448  modremain  16571  ndvdsadd  16573  rpexp12i  16893  isdrngd  21015  isdrngdOLD  21017  cramerimp  22997  tsmsxp  24467  xblcntrps  24722  xblcntr  24723  rrxmet  25722  nvaddsub4  31252  hvmulcan2  31668  adjlnop  32681  rrnmet  38743  lfladd  40103  lflsub  40104  lshpset2N  40156  atcvrj1  40468  athgt  40493  ltrncnvel  41179  trlcnv  41202  trljat2  41204  cdlemc5  41232  trlcoabs  41758  trlcolem  41763  dicvaddcl  42227  limsupre3uzlem  46714  fourierdlem42  47128  ovnhoilem2  47581  lincext3  49537