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  7159  frfi  9188  ressress  17208  funcestrcsetclem9  18105  funcsetcestrclem9  18120  latjjdir  18449  grprcan  18940  grpsubrcan  18988  grpaddsubass  18997  mhmmnd  19031  zntoslem  21546  ipdir  21629  ipass  21635  qustgpopn  24095  extwwlkfab  30437  grpomuldivass  30627  nvmdi  30734  dmdsl3  32401  dvrcan5  33312  imaslmod  33428  idlsrgmnd  33589  esum2d  34253  voliune  34389  btwnconn1lem7  36291  poimirlem4  37959  cvrnbtwn4  39739  paddasslem14  40293  paddasslem17  40296  paddss  40305  pmod1i  40308  cdleme1  40687  cdleme2  40688  xlimbr  46273  sbgoldbst  48266  funcringcsetcALTV2lem9  48786  funcringcsetclem9ALTV  48809