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

Theorem ad2ant2l 777
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 747 . 2 ((𝜑 ∧ (𝜏𝜓)) → 𝜒)
32adantll 745 1 (((𝜃𝜑) ∧ (𝜏𝜓)) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382
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 195  df-an 384
This theorem is referenced by:  funcnvqp  5851  mpteqb  6191  mpt2fun  6637  soxp  7154  wfrlem4  7282  oaass  7505  undifixp  7807  undom  7910  xpdom2  7917  tcrank  8607  inawinalem  9367  addcanpr  9724  ltsosr  9771  1re  9895  add42  10108  muladd  10313  mulsub  10324  divmuleq  10581  ltmul12a  10730  lemul12b  10731  lemul12a  10732  mulge0b  10744  qaddcl  11638  qmulcl  11640  iooshf  12081  fzass4  12207  elfzomelpfzo  12395  modid  12514  cshwleneq  13362  s2eq2seq  13480  tanaddlem  14683  fpwipodrs  16935  issubg4  17384  ghmpreima  17453  cntzsubg  17540  symgfixf1  17628  islmodd  18640  lssvsubcl  18713  lssvscl  18724  lmhmf1o  18815  pwsdiaglmhm  18826  lmimco  19949  scmatghm  20105  scmatmhm  20106  mat2pmatscmxcl  20311  fctop  20565  cctop  20567  opnneissb  20675  pnrmopn  20904  hausnei2  20914  neitx  21167  txcnmpt  21184  txrest  21191  tx1stc  21210  fbssfi  21398  opnfbas  21403  rnelfmlem  21513  alexsubALTlem3  21610  metcnp3  22102  cncfmet  22466  evth  22513  caucfil  22833  ovolun  23018  dveflem  23490  efnnfsumcl  24573  efchtdvds  24629  lgsdir2  24799  axdimuniq  25538  axcontlem2  25590  friendship  26442  hvsub4  27071  his35  27122  shscli  27353  5oalem2  27691  3oalem2  27699  hosub4  27849  hmops  28056  hmopm  28057  hmopco  28059  adjmul  28128  adjadd  28129  mdslmd1lem1  28361  mdslmd1lem2  28362  elmrsubrn  30464  dfon2lem6  30730  nofulllem4  30897  funline  31212  neibastop2lem  31318  isbasisrelowllem1  32162  isbasisrelowllem2  32163  mbfposadd  32410  itg2addnc  32417  fdc  32494  seqpo  32496  ismtyval  32552  paddss12  33906  mzpcompact2lem  36115  jm2.26  36370  fmtnofac2lem  39802  av-friendship  41534  rnghmsubcsetclem2  41749  rhmsubcsetclem2  41795  rhmsubcrngclem2  41801  zlmodzxzsubm  41911  ltsubaddb  42079  ltsubsubb  42080
  Copyright terms: Public domain W3C validator