Theorem 3ad2antl2 1184

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1085

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 396  df-3an 1087

This theorem is referenced by:  simpl2  1190  simpl2l  1224  simpl2r  1225  simpl21  1249  simpl22  1250  simpl23  1251  fcofo  7297  cocan1  7300  ordiso2  9538  fin1a2lem9  10431  fin1a2lem12  10434  gchpwdom  10693  winainflem  10716  bpolydif  16031  dvdsmodexp  16238  muldvds1  16257  lcmdvds  16578  ramcl  16997  oddvdsnn0  19498  ghmplusg  19800  frlmsslss2  21708  frlmsslsp  21729  islindf4  21771  mamures  22291  matepmcl  22363  matepm2cl  22364  pmatcollpw2lem  22678  cnpnei  23167  ssref  23415  qtopss  23618  elfm2  23851  flffbas  23898  cnpfcf  23944  deg1ldg  26027  brbtwn2  28715  colinearalg  28720  axsegconlem1  28727  upgrpredgv  28951  cusgrrusgr  29394  upgrewlkle2  29419  wwlksm1edg  29691  clwwlkf  29856  wwlksext2clwwlk  29866  nvmul0or  30459  hoadddi  31612  volfiniune  33849  bnj548  34528  funsseq  35363  nn0prpwlem  35806  fnemeet1  35850  curfv  37073  lindsadd  37086  keridl  37505  pmapglbx  39242  elpaddn0  39273  paddasslem9  39301  paddasslem10  39302  cdleme42mgN  39961  factwoffsmonot  41694  relexpxpmin  43147  ntrclsk3  43500  n0p  44407  wessf1ornlem  44558  infxr  44749  lptre2pt  45028  dvnprodlem1  45334  fourierdlem42  45537  fourierdlem48  45542  fourierdlem54  45548  fourierdlem77  45571  sge0rpcpnf  45809  hoicvr  45936  smflimsuplem7  46214