Theorem 3ad2antr3 1187

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

Syntax hints:   → wi 4   ∧ wa 394   ∧ w3a 1084

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 206  df-an 395  df-3an 1086

This theorem is referenced by:  simpr3  1193  simpr3l  1231  simpr3r  1232  simpr31  1260  simpr32  1261  simpr33  1262  fpr2g  7227  frfi  9317  ressress  17234  funcestrcsetclem9  18144  funcsetcestrclem9  18159  latjjdir  18489  grprcan  18935  grpsubrcan  18982  grpaddsubass  18991  mhmmnd  19025  zntoslem  21495  ipdir  21576  ipass  21582  qustgpopn  24042  extwwlkfab  30180  grpomuldivass  30369  nvmdi  30476  dmdsl3  32143  dvrcan5  32962  imaslmod  33083  idlsrgmnd  33243  esum2d  33717  voliune  33853  btwnconn1lem7  35694  poimirlem4  37102  cvrnbtwn4  38755  paddasslem14  39310  paddasslem17  39313  paddss  39322  pmod1i  39325  cdleme1  39704  cdleme2  39705  xlimbr  45217  sbgoldbst  47120  funcringcsetcALTV2lem9  47411  funcringcsetclem9ALTV  47434