Theorem 3ad2antr2 1189

Description: Deduction adding conjuncts to antecedent. (Contributed by NM, 27-Dec-2007.)

Hypothesis

Ref	Expression
3ad2antl.1	⊢ ((𝜑 ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
3ad2antr2	⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜏)) → 𝜃)

Proof of Theorem 3ad2antr2

Step	Hyp	Ref	Expression
1		3ad2antl.1	. . 3 ⊢ ((𝜑 ∧ 𝜒) → 𝜃)
2	1	adantrl 714	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)
3	2	3adantr3 1171	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜏)) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 397   ∧ 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 206  df-an 398  df-3an 1089

This theorem is referenced by:  simpr2  1195  simpr2l  1232  simpr2r  1233  simpr21  1260  simpr22  1261  simpr23  1262  wereu  5596  axdc4lem  10257  ioc0  13172  funcestrcsetclem9  17910  funcsetcestrclem9  17925  grpsubadd  18708  zntoslem  20809  psrbaglesuppOLD  21173  mdsl3  30723  dvrcan5  31535  idlsrgmnd  31704  prv1n  33438  brofs2  34424  brifs2  34425  poimirlem28  35849  ftc1anc  35902  frinfm  35937  welb  35938  fdc  35947  unichnidl  36233  cvrnbtwn2  37331  islpln2a  37604  paddss1  37873  paddss2  37874  paddasslem17  37892  tendospass  39075  funcringcsetcALTV2lem9  45660  funcringcsetclem9ALTV  45683  ldepsprlem  45871