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  7185  frfi  9232  ressress  17217  funcestrcsetclem9  18109  funcsetcestrclem9  18124  latjjdir  18451  grprcan  18905  grpsubrcan  18953  grpaddsubass  18962  mhmmnd  18996  zntoslem  21466  ipdir  21548  ipass  21554  qustgpopn  24007  extwwlkfab  30281  grpomuldivass  30470  nvmdi  30577  dmdsl3  32244  dvrcan5  33187  imaslmod  33324  idlsrgmnd  33485  esum2d  34083  voliune  34219  btwnconn1lem7  36081  poimirlem4  37618  cvrnbtwn4  39272  paddasslem14  39827  paddasslem17  39830  paddss  39839  pmod1i  39842  cdleme1  40221  cdleme2  40222  xlimbr  45825  sbgoldbst  47776  funcringcsetcALTV2lem9  48283  funcringcsetclem9ALTV  48306