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

Theorem impd 446
Description: Importation deduction. (Contributed by NM, 31-Mar-1994.)
Hypothesis
Ref Expression
impd.1 (𝜑 → (𝜓 → (𝜒𝜃)))
Assertion
Ref Expression
impd (𝜑 → ((𝜓𝜒) → 𝜃))

Proof of Theorem impd
StepHypRef Expression
1 impd.1 . . . 4 (𝜑 → (𝜓 → (𝜒𝜃)))
21com3l 89 . . 3 (𝜓 → (𝜒 → (𝜑𝜃)))
32imp 444 . 2 ((𝜓𝜒) → (𝜑𝜃))
43com12 32 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:  imp32  448  pm3.31  460  syland  499  imp4b  614  imp4c  618  imp4d  619  imp5d  626  expimpd  630  expl  649  3expib  1117  ax13lem1  2393  equs5  2488  rsp2  3074  moi  3530  reu6  3536  sbciegft  3607  elpwunsn  4368  prel12OLD  4527  opthpr  4528  preqsnd  4536  opthprneg  4545  3elpr2eq  4587  invdisj  4790  reusv1OLD  5016  ralxfrd  5028  ralxfrd2  5033  sotr2  5216  wefrc  5260  relop  5428  elres  5593  iss  5605  tz7.7  5910  ordtr2  5929  funssres  6091  fv3  6368  funopsn  6577  fmptsnd  6600  tpres  6631  funfvima  6656  isomin  6751  sorpsscmpl  7114  peano5  7255  f1oweALT  7318  poxp  7458  soxp  7459  wfr3g  7583  tfr3  7665  tz7.48-1  7708  omordi  7817  odi  7830  omass  7831  oen0  7837  nndi  7874  nnmass  7875  nnmordi  7882  nnmord  7883  eroveu  8011  findcard3  8370  fiint  8404  suplub  8533  hartogs  8616  card2on  8626  unxpwdom2  8660  inf3lem2  8701  epfrs  8782  tcel  8796  dfac2b  9163  dfac2OLD  9165  cfcoflem  9306  infpssr  9342  isf32lem9  9395  axdc3lem4  9487  axcclem  9491  zorn2lem7  9536  ttukeylem6  9548  brdom6disj  9566  ondomon  9597  inar1  9809  gruen  9846  indpi  9941  nqereu  9963  genpn0  10037  distrlem1pr  10059  distrlem5pr  10061  ltexprlem1  10070  reclem4pr  10084  addsrmo  10106  mulsrmo  10107  supsrlem  10144  lelttr  10340  ltletr  10341  ltlen  10350  mulgt1  11094  fzind  11687  eqreznegel  11987  xrlelttr  12200  xrltletr  12201  xnn0xaddcl  12279  fzen  12571  elfzodifsumelfzo  12748  bernneq  13204  fundmge2nop0  13486  swrdswrdlem  13679  wrd2ind  13697  reuccats1lem  13699  swrdccatin1  13703  repsdf2  13745  limsupbnd2  14433  rlimuni  14500  mulcn2  14545  rlimno1  14603  prodmolem2  14884  dvdsmod0  15208  ndvdssub  15355  lcmfunsnlem1  15572  lcmfunsnlem2  15575  coprmdvds  15588  coprmdvdsOLD  15589  coprmdvds2  15590  divgcdcoprm0  15601  maxprmfct  15643  pceu  15773  dvdsprmpweqnn  15811  oddprmdvds  15829  infpnlem1  15836  prmgaplem6  15982  imasaddfnlem  16410  initoeu1  16882  termoeu1  16889  plelttr  17193  gsumval2a  17500  symgfix2  18056  gsmsymgrfixlem1  18067  psgnunilem4  18137  lsmmod  18308  lsmdisj2  18315  efgrelexlemb  18383  pgpfac1lem5  18698  lindfrn  20382  mat1dimcrng  20505  dmatelnd  20524  mdetunilem7  20646  cpmatacl  20743  cpmatmcllem  20745  chfacfisf  20881  chfacfisfcpmat  20882  lmss  21324  lmcnp  21330  hausnei2  21379  isnrm2  21384  isnrm3  21385  cmpsublem  21424  2ndcdisj  21481  1stccnp  21487  txcnpi  21633  txlm  21673  tx1stc  21675  fgss2  21899  fgfil  21900  fgcl  21903  ufileu  21944  rnelfm  21978  fmfnfmlem2  21980  fmfnfmlem4  21982  fmfnfm  21983  ufilcmp  22057  cnpfcf  22066  alexsubALTlem2  22073  alexsubALTlem4  22075  alexsubALT  22076  tmdgsum2  22121  tsmsxp  22179  prdsxmslem2  22555  ivthlem2  23441  ivthlem3  23442  ovolicc2  23510  volfiniun  23535  dyadmax  23586  ellimc3  23862  dvlip2  23977  dvne0  23993  zabsle1  25241  2lgslem3  25349  axcontlem4  26067  umgrislfupgrlem  26237  uhgr2edg  26320  ushgredgedg  26341  ushgredgedgloop  26343  nb3grprlem1  26501  rusgr1vtx  26715  wlkv0  26778  wlkonl1iedg  26792  uhgrwkspthlem2  26881  usgr2wlkneq  26883  usgr2trlncl  26887  uspgrn2crct  26932  wspthsnonn0vne  27058  umgrwwlks2on  27099  elwspths2on  27102  clwlkclwwlkf1lem3  27150  erclwwlktr  27166  erclwwlkntr  27223  frgrnbnb  27468  frgr2wwlk1  27504  frrusgrord  27516  wlkl0  27549  frgrregord013  27584  isch3  28428  ocin  28485  shmodsi  28578  spansneleq  28759  stj  29424  atom1d  29542  atcvat2i  29576  chirredlem1  29579  chirredi  29583  mdsymlem3  29594  mdsymlem6  29597  bnj849  31323  pconnconn  31541  cvmsss2  31584  cvmliftlem7  31601  mclsind  31795  dfpo2  31973  dfon2lem9  32022  dfon2  32023  frr3g  32106  scutun12  32244  cgrextend  32442  btwntriv2  32446  btwncomim  32447  btwnexch3  32454  funtransport  32465  ifscgr  32478  colinearxfr  32509  lineext  32510  fscgr  32514  outsideoftr  32563  trer  32637  finminlem  32639  fnessref  32679  fgmin  32692  bj-andnotim  32901  bj-alanim  32924  bj-0int  33379  relowlssretop  33540  finxpsuclem  33563  wl-ax13lem1  33618  poimirlem29  33769  itg2addnclem3  33794  itg2addnc  33795  areacirc  33836  ismtybndlem  33936  heibor1lem  33939  iss2  34453  prtlem17  34683  riotasvd  34763  lshpsmreu  34917  atnle  35125  cvratlem  35228  cvrat2  35236  3dim1  35274  2llnjN  35374  2lplnj  35427  linepsubN  35559  pmapsub  35575  paddasslem14  35640  pclfinN  35707  ispsubcl2N  35754  pclfinclN  35757  ldilval  35920  trlord  36377  cdlemk36  36721  dihlsscpre  37043  baerlem3lem2  37519  baerlem5alem2  37520  baerlem5blem2  37521  pellexlem5  37917  pellex  37919  pell1234qrmulcl  37939  pellfundex  37970  relexpmulnn  38521  clsk1indlem3  38861  19.41rg  39286  iunconnlem2  39688  nltle2tri  41851  iccpartnel  41902  fmtnofac2lem  42008  sfprmdvdsmersenne  42048  lighneallem3  42052  lighneallem4  42055  bgoldbtbnd  42225  upgrwlkupwlk  42249  nzerooringczr  42600  ldepspr  42790  aacllem  43078
  Copyright terms: Public domain W3C validator