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 716	. 2 ⊢ ((𝜑 ∧ (𝜏 ∧ 𝜒)) → 𝜃)
3	2	3adantr1 1170	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜏 ∧ 𝜒)) → 𝜃)

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

This theorem is referenced by:  simpr3  1197  simpr3l  1235  simpr3r  1236  simpr31  1264  simpr32  1265  simpr33  1266  fpr2g  7147  frfi  9174  ressress  17158  funcestrcsetclem9  18054  funcsetcestrclem9  18069  latjjdir  18398  grprcan  18852  grpsubrcan  18900  grpaddsubass  18909  mhmmnd  18943  zntoslem  21463  ipdir  21546  ipass  21552  qustgpopn  24005  extwwlkfab  30296  grpomuldivass  30485  nvmdi  30592  dmdsl3  32259  dvrcan5  33176  imaslmod  33290  idlsrgmnd  33451  esum2d  34060  voliune  34196  btwnconn1lem7  36067  poimirlem4  37604  cvrnbtwn4  39258  paddasslem14  39812  paddasslem17  39815  paddss  39824  pmod1i  39827  cdleme1  40206  cdleme2  40207  xlimbr  45808  sbgoldbst  47762  funcringcsetcALTV2lem9  48282  funcringcsetclem9ALTV  48305