Theorem 3ad2antl2 1186

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

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

This theorem is referenced by:  simpl2  1192  simpl2l  1226  simpl2r  1227  simpl21  1251  simpl22  1252  simpl23  1253  fcofo  7288  cocan1  7291  ordiso2  9512  fin1a2lem9  10405  fin1a2lem12  10408  gchpwdom  10667  winainflem  10690  bpolydif  16001  dvdsmodexp  16207  muldvds1  16226  lcmdvds  16547  ramcl  16964  oddvdsnn0  19414  ghmplusg  19716  frlmsslss2  21336  frlmsslsp  21357  islindf4  21399  mamures  21899  matepmcl  21971  matepm2cl  21972  pmatcollpw2lem  22286  cnpnei  22775  ssref  23023  qtopss  23226  elfm2  23459  flffbas  23506  cnpfcf  23552  deg1ldg  25617  brbtwn2  28201  colinearalg  28206  axsegconlem1  28213  upgrpredgv  28437  cusgrrusgr  28876  upgrewlkle2  28901  wwlksm1edg  29173  clwwlkf  29338  wwlksext2clwwlk  29348  nvmul0or  29941  hoadddi  31094  volfiniune  33297  bnj548  33977  funsseq  34808  nn0prpwlem  35293  fnemeet1  35337  curfv  36554  lindsadd  36567  keridl  36986  pmapglbx  38726  elpaddn0  38757  paddasslem9  38785  paddasslem10  38786  cdleme42mgN  39445  factwoffsmonot  41109  relexpxpmin  42550  ntrclsk3  42903  n0p  43812  wessf1ornlem  43963  infxr  44156  lptre2pt  44435  dvnprodlem1  44741  fourierdlem42  44944  fourierdlem48  44949  fourierdlem54  44955  fourierdlem77  44978  sge0rpcpnf  45216  hoicvr  45343  smflimsuplem7  45621  isomgrsym  46583