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

Theorem adantld 484
Description: Deduction adding a conjunct to the left of an antecedent. (Contributed by NM, 4-May-1994.) (Proof shortened by Wolf Lammen, 20-Dec-2012.)
Hypothesis
Ref Expression
adantld.1 (𝜑 → (𝜓𝜒))
Assertion
Ref Expression
adantld (𝜑 → ((𝜃𝜓) → 𝜒))

Proof of Theorem adantld
StepHypRef Expression
1 simpr 479 . 2 ((𝜃𝜓) → 𝜓)
2 adantld.1 . 2 (𝜑 → (𝜓𝜒))
31, 2syl5 34 1 (𝜑 → ((𝜃𝜓) → 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383
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 197  df-an 385
This theorem is referenced by:  jaoa  533  dedlema  1032  dedlemb  1033  prlem1  1043  2eu3  2693  unineq  4020  3elpr2eq  4587  tz7.7  5910  ordsssuc2  5975  fpropnf1  6687  nnsuc  7247  el2mpt2csbcl  7418  poxp  7457  suppimacnv  7474  ressuppss  7482  imacosupp  7504  onnseq  7610  tz7.49  7709  oaass  7810  omordi  7815  nnmordi  7880  eroprf  8012  xpdom2  8220  inf3lem2  8699  trcl  8777  r1pwss  8820  cardaleph  9102  dfac2b  9143  dfac2OLD  9145  axcc4  9453  acncc  9454  zorn2lem7  9516  iundom2g  9554  cfpwsdom  9598  grothomex  9843  ltexprlem2  10051  1re  10231  00id  10403  mulge0  10738  nn0ge2m1nn  11552  xrlttr  12166  xmullem2  12288  snunioo  12491  fzen  12551  eluzgtdifelfzo  12724  ssfzo12bi  12757  modirr  12935  hash2pr  13443  hash3tr  13464  cshf1  13756  cshweqrep  13767  limsupbnd2  14413  climrlim2  14477  climuni  14482  mulcn2  14525  serf0  14610  cvgcmp  14747  ntrivcvg  14828  smuval2  15406  dfgcd2  15465  lcmgcdlem  15521  lcmdvds  15523  lcmf  15548  qnumdencl  15649  infpnlem1  15816  ram0  15928  prmgaplem6  15962  prmgaplem7  15963  prmlem1  16016  prmlem2  16029  setsstruct  16100  catass  16548  inveq  16635  sscfn1  16678  catsubcat  16700  subccocl  16706  funcco  16732  initoeu2  16867  funcestrcsetclem8  16988  funcsetcestrclem8  17003  gsmsymgrfixlem1  18047  psgnran  18135  efgi  18332  efgi2  18338  cntzcmnss  18446  telgsumfzs  18586  dprddisj2  18638  prmirredlem  20043  psgnghm  20128  scmatghm  20541  cpmatacl  20723  pm2mpf1  20806  fvmptnn04if  20856  lmcls  21308  isfild  21863  flffbas  22000  cnpflf2  22005  qustgplem  22125  tngngp3  22661  reperflem  22822  nmhmcn  23120  iscau2  23275  iscmet3lem2  23290  ivthlem2  23421  ovolmge0  23445  itg2seq  23708  limciun  23857  dveflem  23941  lhop1  23976  ftc1lem6  24003  mdegnn0cl  24030  aalioulem6  24291  lgsqrmod  25276  gausslemma2dlem3  25292  pntlem3  25497  axlowdimlem16  26036  axcontlem12  26054  umgrislfupgrlem  26216  uhgr2edg  26299  ushgredgedg  26320  ushgredgedgloop  26322  nbuhgr2vtx1edgb  26447  edgnbusgreu  26467  usgredgsscusgredg  26565  wlkdlem2  26790  pthdivtx  26835  upgrwlkdvdelem  26842  spthonepeq  26858  pthdlem1  26872  wwlksnprcl  26942  wlknewwlksn  26996  clwlkclwwlklem2a4  27120  clwlkclwwlklem2  27123  clwwlkwwlksb  27184  clwwlknun  27261  clwwlknunOLD  27265  uhgr3cyclexlem  27333  eucrctshift  27395  frgrncvvdeqlem2  27454  frgrncvvdeqlem9  27461  numclwlk1lem2foa  27513  numclwlk1lem2f1  27516  ubthlem2  28036  shsvs  28491  mdsl2i  29490  mdsl2bi  29491  mdslmd1lem1  29493  atss  29514  chcv1  29523  chrelat2i  29533  atexch  29549  cdj3lem1  29602  bian1d  29615  disjxpin  29708  fpwrelmap  29817  nn0min  29876  sigaclci  30504  dya2iocuni  30654  omssubadd  30671  subfacp1lem6  31474  mthmblem  31784  dfon2lem6  31998  dfrdg4  32364  altopth2  32379  cgrtriv  32415  cgrextend  32421  lineext  32489  btwnconn1  32514  colinbtwnle  32531  trer  32616  elicc3  32617  poimirlem27  33749  poimirlem29  33751  poimir  33755  itg2addnc  33777  ftc1cnnc  33797  areacirclem1  33813  prnc  34179  ispridlc  34182  lcvexchlem4  34827  lcvexchlem5  34828  lkrss2N  34959  cvrnbtwn  35061  hlrelat2  35192  atle  35225  lvolex3N  35327  lplnnlelln  35332  llncvrlpln2  35346  lvolnlelln  35373  lvolnlelpln  35374  lplncvrlvol2  35404  snatpsubN  35539  linepsubN  35541  pmodlem2  35636  linepsubclN  35740  dihatexv  37129  eldioph2b  37828  pell1234qrreccl  37920  islssfg2  38143  hbtlem2  38196  clss2lem  38420  clsk1indlem3  38843  sspwtrALT2  39557  2reu3  41694  iccpartres  41864  iccpartiltu  41868  icceuelpart  41882  goldbachthlem2  41968  lighneallem4  42037  sbgoldbwt  42175  sbgoldbst  42176  nnsum4primesoddALTV  42195  nnsum4primeseven  42198  nnsum4primesevenALTV  42199  bgoldbtbndlem2  42204  sprsymrelfvlem  42250  mgmpropd  42285  rnghmsubcsetclem2  42486  funcrngcsetc  42508  rhmsubcsetclem2  42532  rhmsubcrngclem2  42538  funcringcsetc  42545  srhmsubc  42586  rhmsubclem4  42599  srhmsubcALTV  42604  rhmsubcALTVlem4  42617  ztprmneprm  42635  pgrpgt2nabl  42657  snlindsntor  42770  elbigo2  42856
  Copyright terms: Public domain W3C validator