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

Theorem impd 445
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 86 . . 3 (𝜓 → (𝜒 → (𝜑𝜃)))
32imp 443 . 2 ((𝜓𝜒) → (𝜑𝜃))
43com12 32 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:  imp32  447  pm3.31  459  syland  496  imp4b  610  imp4c  614  imp4d  615  imp5d  622  expimpd  626  expl  645  3expib  1259  ax13lem1  2235  equs5  2338  rsp2  2919  moi  3355  reu6  3361  sbciegft  3432  elpwunsn  4170  prel12  4318  opthpr  4319  invdisj  4565  reusv1OLD  4788  ralxfrd  4800  ralxfrd2  4805  sotr2  4978  wefrc  5022  relop  5182  elres  5342  iss  5354  tz7.7  5652  ordtr2  5671  funssres  5830  fv3  6101  fmptsnd  6318  tpres  6349  funfvima  6374  isomin  6465  sorpsscmpl  6823  peano5  6958  f1oweALT  7020  poxp  7153  soxp  7154  wfr3g  7277  tfr3  7359  tz7.48-1  7402  omordi  7510  odi  7523  omass  7524  oen0  7530  nndi  7567  nnmass  7568  nnmordi  7575  nnmord  7576  eroveu  7706  findcard3  8065  fiint  8099  suplub  8226  hartogs  8309  card2on  8319  unxpwdom2  8353  inf3lem2  8386  epfrs  8467  tcel  8481  dfac2  8813  cfcoflem  8954  infpssr  8990  isf32lem9  9043  axdc3lem4  9135  axcclem  9139  zorn2lem7  9184  ttukeylem6  9196  brdom6disj  9212  ondomon  9241  inar1  9453  gruen  9490  indpi  9585  nqereu  9607  genpn0  9681  distrlem1pr  9703  distrlem5pr  9705  ltexprlem1  9714  reclem4pr  9728  addsrmo  9750  mulsrmo  9751  supsrlem  9788  lelttr  9979  ltletr  9980  ltlen  9989  mulgt1  10731  fzind  11307  eqreznegel  11606  xrlelttr  11822  xrltletr  11823  fzen  12184  elfzodifsumelfzo  12356  bernneq  12807  swrdswrdlem  13257  wrd2ind  13275  reuccats1lem  13277  swrdccatin1  13280  repsdf2  13322  limsupbnd2  14008  rlimuni  14075  mulcn2  14120  rlimno1  14178  prodmolem2  14450  ndvdssub  14917  lcmfunsnlem1  15134  lcmfunsnlem2  15137  coprmdvds  15150  coprmdvdsOLD  15151  coprmdvds2  15152  divgcdcoprm0  15163  maxprmfct  15205  pceu  15335  dvdsprmpweqnn  15373  oddprmdvds  15391  infpnlem1  15398  prmgaplem6  15544  imasaddfnlem  15957  initoeu1  16430  termoeu1  16437  plelttr  16741  gsumval2a  17048  symgfix2  17605  gsmsymgrfixlem1  17616  psgnunilem4  17686  lsmmod  17857  lsmdisj2  17864  efgrelexlemb  17932  pgpfac1lem5  18247  lindfrn  19921  mat1dimcrng  20044  dmatelnd  20063  mdetunilem7  20185  cpmatacl  20282  cpmatmcllem  20284  chfacfisf  20420  chfacfisfcpmat  20421  lmss  20854  lmcnp  20860  hausnei2  20909  isnrm2  20914  isnrm3  20915  cmpsublem  20954  2ndcdisj  21011  1stccnp  21017  txcnpi  21163  txlm  21203  tx1stc  21205  fgss2  21430  fgfil  21431  fgcl  21434  ufileu  21475  rnelfm  21509  fmfnfmlem2  21511  fmfnfmlem4  21513  fmfnfm  21514  ufilcmp  21588  cnpfcf  21597  alexsubALTlem2  21604  alexsubALTlem4  21606  alexsubALT  21607  tmdgsum2  21652  tsmsxp  21710  prdsxmslem2  22085  ivthlem2  22945  ivthlem3  22946  ovolicc2  23014  volfiniun  23039  dyadmax  23089  ellimc3  23366  dvlip2  23479  dvne0  23495  zabsle1  24738  2lgslem3  24846  axcontlem4  25565  usgra2edg  25677  usgrares1  25705  nb3graprlem1  25746  iswlkg  25818  usgrcyclnl1  25934  nvnencycllem  25937  3v3e3cycl1  25938  4cycl4v4e  25960  4cycl4dv4e  25962  wwlknred  26017  erclwwlktr  26109  erclwwlkntr  26121  clwlkfoclwwlk  26138  el2wlkonotot0  26165  frg2woteq  26353  numclwwlkovf2ex  26379  frgraregord013  26411  isch3  27288  ocin  27345  shmodsi  27438  spansneleq  27619  stj  28284  atom1d  28402  atcvat2i  28436  chirredlem1  28439  chirredi  28443  mdsymlem3  28454  mdsymlem6  28457  bnj849  30055  pconcon  30273  cvmsss2  30316  cvmliftlem7  30333  mclsind  30527  dfpo2  30704  dfon2lem9  30746  dfon2  30747  frr3g  30829  frrlem11  30842  cgrextend  31091  btwntriv2  31095  btwncomim  31096  btwnexch3  31103  funtransport  31114  ifscgr  31127  colinearxfr  31158  lineext  31159  fscgr  31163  outsideoftr  31212  trer  31286  finminlem  31288  fnessref  31328  fgmin  31341  bj-andnotim  31552  bj-alanim  31587  relowlssretop  32183  finxpsuclem  32206  wl-ax13lem1  32262  poimirlem29  32404  itg2addnclem3  32429  itg2addnc  32430  areacirc  32471  ismtybndlem  32571  heibor1lem  32574  prtlem17  32975  riotasvd  33056  lshpsmreu  33210  atnle  33418  cvratlem  33521  cvrat2  33529  3dim1  33567  2llnjN  33667  2lplnj  33720  linepsubN  33852  pmapsub  33868  paddasslem14  33933  pclfinN  34000  ispsubcl2N  34047  pclfinclN  34050  ldilval  34213  trlord  34671  cdlemk36  35015  dihlsscpre  35337  baerlem3lem2  35813  baerlem5alem2  35814  baerlem5blem2  35815  pellexlem5  36211  pellex  36213  pell1234qrmulcl  36233  pellfundex  36264  relexpmulnn  36816  clsk1indlem3  37157  19.41rg  37583  iunconlem2  37989  nltle2tri  39740  iccpartnel  39774  fmtnofac2lem  39816  sfprmdvdsmersenne  39856  lighneallem3  39860  lighneallem4  39863  bgoldbtbnd  40023  funopsn  40137  fundmge2nop0  40145  xnn0xaddcl  40208  umgrislfupgrlem  40342  uhgr2edg  40430  ushgredgedga  40451  ushgredgedgaloop  40453  nb3grprlem1  40603  rusgr1vtx  40783  upgr1wlkwlk  40842  1wlkv0  40854  wlkOnl1iedg  40868  sPthdifv  40934  uhgr1wlkspthlem2  40955  usgr2wlkneq  40957  usgr2trlncl  40961  usgr2pth  40965  cyclnsPth  41001  uspgrn2crct  41006  wspthsnonn0vne  41119  wwlks2onv  41153  umgrwwlks2on  41156  elwspths2on  41158  erclwwlkstr  41238  erclwwlksntr  41250  frgrnbnb  41458  av-numclwwlkovf2ex  41512  av-frgraregord013  41544  nzerooringczr  41859  ldepspr  42051  aacllem  42312
  Copyright terms: Public domain W3C validator