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

Theorem ad2ant2l 743
Description: Deduction adding two conjuncts to antecedent. (Contributed by NM, 8-Jan-2006.)
Hypothesis
Ref Expression
ad2ant2.1 ((𝜑𝜓) → 𝜒)
Assertion
Ref Expression
ad2ant2l (((𝜃𝜑) ∧ (𝜏𝜓)) → 𝜒)

Proof of Theorem ad2ant2l
StepHypRef Expression
1 ad2ant2.1 . . 3 ((𝜑𝜓) → 𝜒)
21adantrl 698 . 2 ((𝜑 ∧ (𝜏𝜓)) → 𝜒)
32adantll 696 1 (((𝜃𝜑) ∧ (𝜏𝜓)) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384
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 198  df-an 385
This theorem is referenced by:  funcnvqp  6164  mpteqb  6520  mpt2fun  6992  soxp  7524  wfrlem4  7653  wfrlem4OLD  7654  oaass  7878  undifixp  8181  undom  8287  xpdom2  8294  tcrank  8994  inawinalem  9796  addcanpr  10153  ltsosr  10200  1re  10325  add42  10542  muladd  10747  mulsub  10758  divmuleq  11015  ltmul12a  11164  lemul12b  11165  lemul12a  11166  mulge0b  11178  qaddcl  12023  qmulcl  12025  iooshf  12470  fzass4  12602  elfzomelpfzo  12796  modid  12919  cshwleneq  13787  s2eq2seq  13906  tanaddlem  15116  fpwipodrs  17369  issubg4  17815  ghmpreima  17884  cntzsubg  17970  symgfixf1  18058  islmodd  19073  lssvsubcl  19148  lssvscl  19162  lmhmf1o  19253  pwsdiaglmhm  19264  lmimco  20393  scmatghm  20550  scmatmhm  20551  mat2pmatscmxcl  20758  fctop  21022  cctop  21024  opnneissb  21132  pnrmopn  21361  hausnei2  21371  neitx  21624  txcnmpt  21641  txrest  21648  tx1stc  21667  fbssfi  21854  opnfbas  21859  rnelfmlem  21969  alexsubALTlem3  22066  metcnp3  22558  cncfmet  22924  evth  22971  caucfil  23293  ovolun  23480  dveflem  23956  efnnfsumcl  25043  efchtdvds  25099  lgsdir2  25269  axdimuniq  26007  axcontlem2  26059  frgrwopreglem5lem  27495  frgrwopreglem5ALT  27497  friendship  27587  hvsub4  28222  his35  28273  shscli  28504  5oalem2  28842  3oalem2  28850  hosub4  29000  hmops  29207  hmopm  29208  hmopco  29210  adjmul  29279  adjadd  29280  mdslmd1lem1  29512  mdslmd1lem2  29513  elmrsubrn  31740  dfon2lem6  32013  funline  32570  neibastop2lem  32676  isbasisrelowllem1  33519  isbasisrelowllem2  33520  mbfposadd  33769  itg2addnc  33776  fdc  33852  seqpo  33854  ismtyval  33910  paddss12  35599  mzpcompact2lem  37816  jm2.26  38070  fmtnofac2lem  42055  rnghmsubcsetclem2  42544  rhmsubcsetclem2  42590  rhmsubcrngclem2  42596  zlmodzxzsubm  42705  ltsubaddb  42872  ltsubsubb  42873
  Copyright terms: Public domain W3C validator