Theorem 3ad2antr3 1190

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 1169	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  1196  simpr3l  1234  simpr3r  1235  simpr31  1263  simpr32  1264  simpr33  1265  fpr2g  7199  frfi  9287  ressress  17253  funcestrcsetclem9  18145  funcsetcestrclem9  18160  latjjdir  18487  grprcan  18941  grpsubrcan  18989  grpaddsubass  18998  mhmmnd  19032  zntoslem  21502  ipdir  21584  ipass  21590  qustgpopn  24043  extwwlkfab  30265  grpomuldivass  30454  nvmdi  30561  dmdsl3  32228  dvrcan5  33149  imaslmod  33286  idlsrgmnd  33447  esum2d  34032  voliune  34168  btwnconn1lem7  36032  poimirlem4  37569  cvrnbtwn4  39218  paddasslem14  39773  paddasslem17  39776  paddss  39785  pmod1i  39788  cdleme1  40167  cdleme2  40168  xlimbr  45786  sbgoldbst  47710  funcringcsetcALTV2lem9  48159  funcringcsetclem9ALTV  48182