Theorem 3ad2antl2 1188

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

Hypothesis

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

Assertion

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

Proof of Theorem 3ad2antl2

Step	Hyp	Ref	Expression
1		3ad2antl.1	. . 3 ⊢ ((𝜑 ∧ 𝜒) → 𝜃)
2	1	adantlr 716	. 2 ⊢ (((𝜑 ∧ 𝜏) ∧ 𝜒) → 𝜃)
3	2	3adantl1 1168	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:  simpl2  1194  simpl2l  1228  simpl2r  1229  simpl21  1253  simpl22  1254  simpl23  1255  fcofo  7244  cocan1  7247  ordiso2  9432  fin1a2lem9  10330  fin1a2lem12  10333  gchpwdom  10593  winainflem  10616  bpolydif  15990  dvdsmodexp  16199  muldvds1  16219  lcmdvds  16547  ramcl  16969  oddvdsnn0  19485  ghmplusg  19787  frlmsslss2  21742  frlmsslsp  21763  islindf4  21805  mamures  22353  matepmcl  22418  matepm2cl  22419  pmatcollpw2lem  22733  cnpnei  23220  ssref  23468  qtopss  23671  elfm2  23904  flffbas  23951  cnpfcf  23997  deg1ldg  26065  brbtwn2  28990  colinearalg  28995  axsegconlem1  29002  upgrpredgv  29224  cusgrrusgr  29667  upgrewlkle2  29692  wwlksm1edg  29966  clwwlkf  30134  wwlksext2clwwlk  30144  nvmul0or  30738  hoadddi  31891  volfiniune  34408  bnj548  35073  funsseq  35984  nn0prpwlem  36538  fnemeet1  36582  curfv  37851  lindsadd  37864  keridl  38283  pmapglbx  40145  elpaddn0  40176  paddasslem9  40204  paddasslem10  40205  cdleme42mgN  40864  relexpxpmin  44073  ntrclsk3  44426  n0p  45405  wessf1ornlem  45544  infxr  45725  lptre2pt  45998  dvnprodlem1  46304  fourierdlem42  46507  fourierdlem48  46512  fourierdlem54  46518  fourierdlem77  46541  sge0rpcpnf  46779  hoicvr  46906  smflimsuplem7  47184