Theorem 3ad2antr3 1191

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 715	. 2 ⊢ ((𝜑 ∧ (𝜏 ∧ 𝜒)) → 𝜃)
3	2	3adantr1 1170	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:  simpr3  1197  simpr3l  1235  simpr3r  1236  simpr31  1264  simpr32  1265  simpr33  1266  fpr2g  7213  frfi  9288  ressress  17193  funcestrcsetclem9  18100  funcsetcestrclem9  18115  latjjdir  18445  grprcan  18858  grpsubrcan  18904  grpaddsubass  18913  mhmmnd  18947  zntoslem  21112  ipdir  21192  ipass  21198  qustgpopn  23624  extwwlkfab  29605  grpomuldivass  29794  nvmdi  29901  dmdsl3  31568  dvrcan5  32385  imaslmod  32468  idlsrgmnd  32628  esum2d  33091  voliune  33227  btwnconn1lem7  35065  poimirlem4  36492  cvrnbtwn4  38149  paddasslem14  38704  paddasslem17  38707  paddss  38716  pmod1i  38719  cdleme1  39098  cdleme2  39099  xlimbr  44543  sbgoldbst  46446  funcringcsetcALTV2lem9  46942  funcringcsetclem9ALTV  46965