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  7243  cocan1  7246  ordiso2  9430  fin1a2lem9  10330  fin1a2lem12  10333  gchpwdom  10593  winainflem  10616  bpolydif  16020  dvdsmodexp  16229  muldvds1  16249  lcmdvds  16577  ramcl  17000  oddvdsnn0  19519  ghmplusg  19821  frlmsslss2  21755  frlmsslsp  21776  islindf4  21818  mamures  22362  matepmcl  22427  matepm2cl  22428  pmatcollpw2lem  22742  cnpnei  23229  ssref  23477  qtopss  23680  elfm2  23913  flffbas  23960  cnpfcf  24006  deg1ldg  26057  brbtwn2  28974  colinearalg  28979  axsegconlem1  28986  upgrpredgv  29208  cusgrrusgr  29650  upgrewlkle2  29675  wwlksm1edg  29949  clwwlkf  30117  wwlksext2clwwlk  30127  nvmul0or  30721  hoadddi  31874  volfiniune  34374  bnj548  35039  funsseq  35950  nn0prpwlem  36504  fnemeet1  36548  curfv  37921  lindsadd  37934  keridl  38353  pmapglbx  40215  elpaddn0  40246  paddasslem9  40274  paddasslem10  40275  cdleme42mgN  40934  relexpxpmin  44144  ntrclsk3  44497  n0p  45476  wessf1ornlem  45615  infxr  45796  lptre2pt  46068  dvnprodlem1  46374  fourierdlem42  46577  fourierdlem48  46582  fourierdlem54  46588  fourierdlem77  46611  sge0rpcpnf  46849  hoicvr  46976  smflimsuplem7  47254