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

Theorem impd 447
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 445 . 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 197  df-an 386
This theorem is referenced by:  imp32  449  pm3.31  461  syland  498  imp4b  612  imp4c  616  imp4d  617  imp5d  624  expimpd  628  expl  647  3expib  1265  ax13lem1  2247  equs5  2350  rsp2  2932  moi  3376  reu6  3382  sbciegft  3453  elpwunsn  4202  prel12  4358  opthpr  4359  invdisj  4611  reusv1OLD  4837  ralxfrd  4849  ralxfrd2  4854  sotr2  5034  wefrc  5078  relop  5242  elres  5404  iss  5416  tz7.7  5718  ordtr2  5737  funssres  5898  fv3  6173  funopsn  6378  fmptsnd  6400  tpres  6431  funfvima  6457  isomin  6552  sorpsscmpl  6913  peano5  7051  f1oweALT  7112  poxp  7249  soxp  7250  wfr3g  7373  tfr3  7455  tz7.48-1  7498  omordi  7606  odi  7619  omass  7620  oen0  7626  nndi  7663  nnmass  7664  nnmordi  7671  nnmord  7672  eroveu  7802  findcard3  8163  fiint  8197  suplub  8326  hartogs  8409  card2on  8419  unxpwdom2  8453  inf3lem2  8486  epfrs  8567  tcel  8581  dfac2  8913  cfcoflem  9054  infpssr  9090  isf32lem9  9143  axdc3lem4  9235  axcclem  9239  zorn2lem7  9284  ttukeylem6  9296  brdom6disj  9314  ondomon  9345  inar1  9557  gruen  9594  indpi  9689  nqereu  9711  genpn0  9785  distrlem1pr  9807  distrlem5pr  9809  ltexprlem1  9818  reclem4pr  9832  addsrmo  9854  mulsrmo  9855  supsrlem  9892  lelttr  10088  ltletr  10089  ltlen  10098  mulgt1  10842  fzind  11435  eqreznegel  11734  xrlelttr  11947  xrltletr  11948  xnn0xaddcl  12025  fzen  12316  elfzodifsumelfzo  12490  bernneq  12946  fundmge2nop0  13229  swrdswrdlem  13413  wrd2ind  13431  reuccats1lem  13433  swrdccatin1  13436  repsdf2  13478  limsupbnd2  14164  rlimuni  14231  mulcn2  14276  rlimno1  14334  prodmolem2  14609  ndvdssub  15076  lcmfunsnlem1  15293  lcmfunsnlem2  15296  coprmdvds  15309  coprmdvdsOLD  15310  coprmdvds2  15311  divgcdcoprm0  15322  maxprmfct  15364  pceu  15494  dvdsprmpweqnn  15532  oddprmdvds  15550  infpnlem1  15557  prmgaplem6  15703  imasaddfnlem  16128  initoeu1  16601  termoeu1  16608  plelttr  16912  gsumval2a  17219  symgfix2  17776  gsmsymgrfixlem1  17787  psgnunilem4  17857  lsmmod  18028  lsmdisj2  18035  efgrelexlemb  18103  pgpfac1lem5  18418  lindfrn  20100  mat1dimcrng  20223  dmatelnd  20242  mdetunilem7  20364  cpmatacl  20461  cpmatmcllem  20463  chfacfisf  20599  chfacfisfcpmat  20600  lmss  21042  lmcnp  21048  hausnei2  21097  isnrm2  21102  isnrm3  21103  cmpsublem  21142  2ndcdisj  21199  1stccnp  21205  txcnpi  21351  txlm  21391  tx1stc  21393  fgss2  21618  fgfil  21619  fgcl  21622  ufileu  21663  rnelfm  21697  fmfnfmlem2  21699  fmfnfmlem4  21701  fmfnfm  21702  ufilcmp  21776  cnpfcf  21785  alexsubALTlem2  21792  alexsubALTlem4  21794  alexsubALT  21795  tmdgsum2  21840  tsmsxp  21898  prdsxmslem2  22274  ivthlem2  23161  ivthlem3  23162  ovolicc2  23230  volfiniun  23255  dyadmax  23306  ellimc3  23583  dvlip2  23696  dvne0  23712  zabsle1  24955  2lgslem3  25063  axcontlem4  25781  umgrislfupgrlem  25946  uhgr2edg  26027  ushgredgedg  26048  ushgredgedgloop  26050  nb3grprlem1  26203  rusgr1vtx  26388  wlkv0  26450  wlkonl1iedg  26464  uhgrwkspthlem2  26553  usgr2wlkneq  26555  usgr2trlncl  26559  uspgrn2crct  26603  wspthsnonn0vne  26716  wwlks2onv  26750  umgrwwlks2on  26753  elwspths2on  26755  erclwwlkstr  26836  erclwwlksntr  26848  frgrnbnb  27055  numclwwlkovf2ex  27109  frgrregord013  27141  isch3  27986  ocin  28043  shmodsi  28136  spansneleq  28317  stj  28982  atom1d  29100  atcvat2i  29134  chirredlem1  29137  chirredi  29141  mdsymlem3  29152  mdsymlem6  29155  bnj849  30756  pconnconn  30974  cvmsss2  31017  cvmliftlem7  31034  mclsind  31228  dfpo2  31406  dfon2lem9  31450  dfon2  31451  frr3g  31533  frrlem11  31546  slttr3  31589  cgrextend  31810  btwntriv2  31814  btwncomim  31815  btwnexch3  31822  funtransport  31833  ifscgr  31846  colinearxfr  31877  lineext  31878  fscgr  31882  outsideoftr  31931  trer  32005  finminlem  32007  fnessref  32047  fgmin  32060  bj-andnotim  32268  bj-alanim  32291  relowlssretop  32882  finxpsuclem  32905  wl-ax13lem1  32958  poimirlem29  33109  itg2addnclem3  33134  itg2addnc  33135  areacirc  33176  ismtybndlem  33276  heibor1lem  33279  prtlem17  33680  riotasvd  33761  lshpsmreu  33915  atnle  34123  cvratlem  34226  cvrat2  34234  3dim1  34272  2llnjN  34372  2lplnj  34425  linepsubN  34557  pmapsub  34573  paddasslem14  34638  pclfinN  34705  ispsubcl2N  34752  pclfinclN  34755  ldilval  34918  trlord  35376  cdlemk36  35720  dihlsscpre  36042  baerlem3lem2  36518  baerlem5alem2  36519  baerlem5blem2  36520  pellexlem5  36916  pellex  36918  pell1234qrmulcl  36938  pellfundex  36969  relexpmulnn  37521  clsk1indlem3  37862  19.41rg  38287  iunconnlem2  38693  nltle2tri  40650  iccpartnel  40702  fmtnofac2lem  40809  sfprmdvdsmersenne  40849  lighneallem3  40853  lighneallem4  40856  bgoldbtbnd  41016  upgrwlkupwlk  41039  nzerooringczr  41390  ldepspr  41580  aacllem  41880
  Copyright terms: Public domain W3C validator