Theorem 3ad2antr3 1198

Description: Deduction adding conjuncts to antecedent. (Contributed by NM, 30-Dec-2007.)

Hypothesis

Ref	Expression
3ad2antl.1	⊢ ((𝜑 ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
3ad2antr3	⊢ ((𝜑 ∧ (𝜓 ∧ 𝜏 ∧ 𝜒)) → 𝜃)

Proof of Theorem 3ad2antr3

Step	Hyp	Ref	Expression
1		3ad2antl.1	. . 3 ⊢ ((𝜑 ∧ 𝜒) → 𝜃)
2	1	adantrl 723	. 2 ⊢ ((𝜑 ∧ (𝜏 ∧ 𝜒)) → 𝜃)
3	2	3adantr1 1177	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:  simpr3  1204  simpr3l  1242  simpr3r  1243  simpr31  1271  simpr32  1272  simpr33  1273  fpr2g  7159  frfi  9189  ressress  17212  funcestrcsetclem9  18109  funcsetcestrclem9  18124  latjjdir  18453  grprcan  18944  grpsubrcan  18992  grpaddsubass  19001  mhmmnd  19035  zntoslem  21535  ipdir  21618  ipass  21624  qustgpopn  24107  extwwlkfab  30444  grpomuldivass  30634  nvmdi  30741  dmdsl3  32408  dvrcan5  33321  imaslmod  33440  idlsrgmnd  33609  esum2d  34289  voliune  34425  btwnconn1lem7  36336  poimirlem4  38006  cvrnbtwn4  39786  paddasslem14  40340  paddasslem17  40343  paddss  40352  pmod1i  40355  cdleme1  40734  cdleme2  40735  xlimbr  46284  sbgoldbst  48283  funcringcsetcALTV2lem9  48803  funcringcsetclem9ALTV  48826