MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  3ad2antl2 Structured version   Visualization version   GIF version

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
StepHypRef Expression
1 3ad2antl.1 . . 3 ((𝜑𝜒) → 𝜃)
21adantlr 714 . 2 (((𝜑𝜏) ∧ 𝜒) → 𝜃)
323adantl1 1164 1 (((𝜓𝜑𝜏) ∧ 𝜒) → 𝜃)
Colors of variables: wff setvar class
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
  Copyright terms: Public domain W3C validator