Theorem 3ad2antr3 1192

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087

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 1089

This theorem is referenced by:  simpr3  1198  simpr3l  1236  simpr3r  1237  simpr31  1265  simpr32  1266  simpr33  1267  fpr2g  7166  frfi  9195  ressress  17217  funcestrcsetclem9  18114  funcsetcestrclem9  18129  latjjdir  18458  grprcan  18949  grpsubrcan  18997  grpaddsubass  19006  mhmmnd  19040  zntoslem  21536  ipdir  21619  ipass  21625  qustgpopn  24085  extwwlkfab  30422  grpomuldivass  30612  nvmdi  30719  dmdsl3  32386  dvrcan5  33297  imaslmod  33413  idlsrgmnd  33574  esum2d  34237  voliune  34373  btwnconn1lem7  36275  poimirlem4  37945  cvrnbtwn4  39725  paddasslem14  40279  paddasslem17  40282  paddss  40291  pmod1i  40294  cdleme1  40673  cdleme2  40674  xlimbr  46255  sbgoldbst  48254  funcringcsetcALTV2lem9  48774  funcringcsetclem9ALTV  48797