Theorem 3ad2antl2 1205

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 728	. 2 ⊢ (((𝜑 ∧ 𝜏) ∧ 𝜒) → 𝜃)
3	2	3adantl1 1185	1 ⊢ (((𝜓 ∧ 𝜑 ∧ 𝜏) ∧ 𝜒) → 𝜃)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  simpl2  1211  simpl2l  1245  simpl2r  1246  simpl21  1270  simpl22  1271  simpl23  1272  fcofo  7327  cocan1  7330  onelfvnef1  8487  curfv  8930  ordiso2  9546  fin1a2lem9  10525  fin1a2lem12  10528  gchpwdom  10794  winainflem  10817  bpolydif  16265  dvdsmodexp  16474  muldvds1  16494  lcmdvds  16827  ramcl  17251  oddvdsnn0  19809  ghmplusg  20111  frlmsslss2  22136  frlmsslsp  22157  islindf4  22199  mamures  22767  matepmcl  22832  matepm2cl  22833  pmatcollpw2lem  23150  cnpnei  23637  ssref  23886  qtopss  24089  elfm2  24322  flffbas  24369  cnpfcf  24415  deg1ldg  26465  brbtwn2  29540  colinearalg  29545  axsegconlem1  29552  upgrpredgv  29774  cusgrrusgr  30219  upgrewlkle2  30244  wwlksm1edg  30527  clwwlkf  30695  wwlksext2clwwlk  30705  nvmul0or  31309  hoadddi  32462  volfiniune  34974  bnj548  35638  funsseq  36748  nn0prpwlem  37325  fnemeet1  37369  lindsadd  38804  keridl  39232  pmapglbx  41092  elpaddn0  41123  paddasslem9  41151  paddasslem10  41152  cdleme42mgN  41811  relexpxpmin  44978  ntrclsk3  45331  n0p  46336  wessf1ornlem  46473  infxr  46651  lptre2pt  46923  dvnprodlem1  47229  fourierdlem42  47432  fourierdlem48  47437  fourierdlem54  47443  fourierdlem77  47466  sge0rpcpnf  47704  hoicvr  47831  smflimsuplem7  48109