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

Theorem impd 398
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 395 . 2 ((𝜓𝜒) → (𝜑𝜃))
43com12 32 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:  imp32  407  imp4b  410  imp4c  412  imp4d  413  imp5d  428  pm3.31  438  expimpd  443  expl  447  syland  592  3expib  1145  ax13lem1  2422  equs5  2509  rsp2  3124  moi  3587  reu6  3593  sbciegft  3664  elpwunsn  4417  prel12OLD  4570  opthpr  4571  preqsnd  4579  opthprneg  4587  3elpr2eq  4629  invdisj  4830  ralxfrd  5077  ralxfrd2  5081  snopeqop  5160  sotr2  5261  wefrc  5305  relop  5474  elinxp  5637  elresOLD  5639  iss  5652  tz7.7  5962  ordtr2  5981  funssres  6144  fv3  6426  funopsn  6637  fmptsnd  6660  tpres  6691  funfvima  6717  isomin  6811  sorpsscmpl  7178  peano5  7319  f1oweALT  7382  poxp  7523  soxp  7524  wfr3g  7648  tfr3  7731  tz7.48-1  7774  omordi  7883  odi  7896  omass  7897  oen0  7903  nndi  7940  nnmass  7941  nnmordi  7948  nnmord  7949  eroveu  8078  findcard3  8442  fiint  8476  suplub  8605  hartogs  8688  card2on  8698  unxpwdom2  8732  inf3lem2  8773  epfrs  8854  tcel  8868  dfac2b  9236  dfac2OLD  9238  cfcoflem  9379  infpssr  9415  isf32lem9  9468  axdc3lem4  9560  axcclem  9564  zorn2lem7  9609  ttukeylem6  9621  brdom6disj  9639  ondomon  9670  inar1  9882  gruen  9919  indpi  10014  nqereu  10036  genpn0  10110  distrlem1pr  10132  distrlem5pr  10134  ltexprlem1  10143  reclem4pr  10157  addsrmo  10179  mulsrmo  10180  supsrlem  10217  lelttr  10413  ltletr  10414  ltlen  10423  mulgt1  11167  fzind  11741  eqreznegel  11993  xrlelttr  12205  xrltletr  12206  xnn0xaddcl  12284  fzen  12581  elfzodifsumelfzo  12758  bernneq  13213  fundmge2nop0  13491  swrdswrdlem  13683  wrd2ind  13701  reuccats1lem  13703  swrdccatin1  13707  repsdf2  13749  limsupbnd2  14437  rlimuni  14504  mulcn2  14549  rlimno1  14607  prodmolem2  14886  dvdsmod0  15209  ndvdssub  15352  lcmfunsnlem1  15569  lcmfunsnlem2  15572  coprmdvds  15585  coprmdvds2  15586  divgcdcoprm0  15597  maxprmfct  15638  pceu  15768  dvdsprmpweqnn  15806  oddprmdvds  15824  infpnlem1  15831  prmgaplem6  15977  imasaddfnlem  16393  initoeu1  16865  termoeu1  16872  plelttr  17177  gsumval2a  17484  symgfix2  18037  gsmsymgrfixlem1  18048  psgnunilem4  18118  lsmmod  18289  lsmdisj2  18296  efgrelexlemb  18364  pgpfac1lem5  18680  lindfrn  20370  mat1dimcrng  20494  dmatelnd  20513  mdetunilem7  20635  cpmatacl  20734  cpmatmcllem  20736  chfacfisf  20872  chfacfisfcpmat  20873  lmss  21316  lmcnp  21322  hausnei2  21371  isnrm2  21376  isnrm3  21377  cmpsublem  21416  2ndcdisj  21473  1stccnp  21479  txcnpi  21625  txlm  21665  tx1stc  21667  fgss2  21891  fgfil  21892  fgcl  21895  ufileu  21936  rnelfm  21970  fmfnfmlem2  21972  fmfnfmlem4  21974  fmfnfm  21975  ufilcmp  22049  cnpfcf  22058  alexsubALTlem2  22065  alexsubALTlem4  22067  alexsubALT  22068  tmdgsum2  22113  tsmsxp  22171  prdsxmslem2  22547  ivthlem2  23433  ivthlem3  23434  ovolicc2  23503  volfiniun  23528  dyadmax  23579  ellimc3  23857  dvlip2  23972  dvne0  23988  zabsle1  25235  2lgslem3  25343  axcontlem4  26061  umgrislfupgrlem  26231  uhgr2edg  26315  ushgredgedg  26336  ushgredgedgloop  26338  ushgredgedgloopOLD  26339  nb3grprlem1  26498  rusgr1vtx  26712  wlkv0  26775  wlkonl1iedg  26789  uhgrwkspthlem2  26878  usgr2wlkneq  26880  usgr2trlncl  26884  uspgrn2crct  26929  wspthsnonn0vne  27057  umgrwwlks2on  27098  elwspths2on  27101  clwlkclwwlkf1lem3  27149  erclwwlktr  27165  erclwwlkntr  27222  frgrnbnb  27468  frgr2wwlk1  27504  frrusgrord  27516  wlkl0  27547  frgrregord013  27583  isch3  28426  ocin  28483  shmodsi  28576  spansneleq  28757  stj  29422  atom1d  29540  atcvat2i  29574  chirredlem1  29577  chirredi  29581  mdsymlem3  29592  mdsymlem6  29595  bnj849  31318  pconnconn  31536  cvmsss2  31579  cvmliftlem7  31596  mclsind  31790  dfpo2  31967  dfon2lem9  32016  dfon2  32017  frr3g  32100  scutun12  32238  cgrextend  32436  btwntriv2  32440  btwncomim  32441  btwnexch3  32448  funtransport  32459  ifscgr  32472  colinearxfr  32503  lineext  32504  fscgr  32508  outsideoftr  32557  trer  32631  finminlem  32633  fnessref  32673  fgmin  32686  bj-andnotim  32888  bj-alanim  32911  bj-0int  33366  relowlssretop  33527  finxpsuclem  33550  wl-ax13lem1  33605  poimirlem29  33751  itg2addnclem3  33775  itg2addnc  33776  areacirc  33817  ismtybndlem  33916  heibor1lem  33919  iss2  34425  prtlem17  34655  riotasvd  34735  lshpsmreu  34889  atnle  35097  cvratlem  35201  cvrat2  35209  3dim1  35247  2llnjN  35347  2lplnj  35400  linepsubN  35532  pmapsub  35548  paddasslem14  35613  pclfinN  35680  ispsubcl2N  35727  pclfinclN  35730  ldilval  35893  trlord  36350  cdlemk36  36694  dihlsscpre  37015  baerlem3lem2  37491  baerlem5alem2  37492  baerlem5blem2  37493  pellexlem5  37899  pellex  37901  pell1234qrmulcl  37921  pellfundex  37952  relexpmulnn  38501  clsk1indlem3  38841  19.41rg  39264  iunconnlem2  39665  dfatcolem  41844  f1oresf1o2  41881  nltle2tri  41898  iccpartnel  41949  fmtnofac2lem  42055  sfprmdvdsmersenne  42095  lighneallem3  42099  lighneallem4  42102  bgoldbtbnd  42272  upgrwlkupwlk  42289  nzerooringczr  42640  ldepspr  42830  aacllem  43118
  Copyright terms: Public domain W3C validator