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  497  imp4b  612  imp4c  616  imp4d  617  imp5d  624  expimpd  628  expl  647  3expib  1287  ax13lem1  2284  equs5  2379  rsp2  2965  moi  3422  reu6  3428  sbciegft  3499  elpwunsn  4256  prel12  4414  opthpr  4415  3elpr2eq  4467  invdisj  4670  reusv1OLD  4897  ralxfrd  4909  ralxfrd2  4914  sotr2  5093  wefrc  5137  relop  5305  elres  5470  iss  5482  tz7.7  5787  ordtr2  5806  funssres  5968  fv3  6244  funopsn  6453  fmptsnd  6476  tpres  6507  funfvima  6532  isomin  6627  sorpsscmpl  6990  peano5  7131  f1oweALT  7194  poxp  7334  soxp  7335  wfr3g  7458  tfr3  7540  tz7.48-1  7583  omordi  7691  odi  7704  omass  7705  oen0  7711  nndi  7748  nnmass  7749  nnmordi  7756  nnmord  7757  eroveu  7885  findcard3  8244  fiint  8278  suplub  8407  hartogs  8490  card2on  8500  unxpwdom2  8534  inf3lem2  8564  epfrs  8645  tcel  8659  dfac2  8991  cfcoflem  9132  infpssr  9168  isf32lem9  9221  axdc3lem4  9313  axcclem  9317  zorn2lem7  9362  ttukeylem6  9374  brdom6disj  9392  ondomon  9423  inar1  9635  gruen  9672  indpi  9767  nqereu  9789  genpn0  9863  distrlem1pr  9885  distrlem5pr  9887  ltexprlem1  9896  reclem4pr  9910  addsrmo  9932  mulsrmo  9933  supsrlem  9970  lelttr  10166  ltletr  10167  ltlen  10176  mulgt1  10920  fzind  11513  eqreznegel  11812  xrlelttr  12025  xrltletr  12026  xnn0xaddcl  12104  fzen  12396  elfzodifsumelfzo  12573  bernneq  13030  fundmge2nop0  13312  swrdswrdlem  13505  wrd2ind  13523  reuccats1lem  13525  swrdccatin1  13529  repsdf2  13571  limsupbnd2  14258  rlimuni  14325  mulcn2  14370  rlimno1  14428  prodmolem2  14709  dvdsmod0  15033  ndvdssub  15180  lcmfunsnlem1  15397  lcmfunsnlem2  15400  coprmdvds  15413  coprmdvdsOLD  15414  coprmdvds2  15415  divgcdcoprm0  15426  maxprmfct  15468  pceu  15598  dvdsprmpweqnn  15636  oddprmdvds  15654  infpnlem1  15661  prmgaplem6  15807  imasaddfnlem  16235  initoeu1  16708  termoeu1  16715  plelttr  17019  gsumval2a  17326  symgfix2  17882  gsmsymgrfixlem1  17893  psgnunilem4  17963  lsmmod  18134  lsmdisj2  18141  efgrelexlemb  18209  pgpfac1lem5  18524  lindfrn  20208  mat1dimcrng  20331  dmatelnd  20350  mdetunilem7  20472  cpmatacl  20569  cpmatmcllem  20571  chfacfisf  20707  chfacfisfcpmat  20708  lmss  21150  lmcnp  21156  hausnei2  21205  isnrm2  21210  isnrm3  21211  cmpsublem  21250  2ndcdisj  21307  1stccnp  21313  txcnpi  21459  txlm  21499  tx1stc  21501  fgss2  21725  fgfil  21726  fgcl  21729  ufileu  21770  rnelfm  21804  fmfnfmlem2  21806  fmfnfmlem4  21808  fmfnfm  21809  ufilcmp  21883  cnpfcf  21892  alexsubALTlem2  21899  alexsubALTlem4  21901  alexsubALT  21902  tmdgsum2  21947  tsmsxp  22005  prdsxmslem2  22381  ivthlem2  23267  ivthlem3  23268  ovolicc2  23336  volfiniun  23361  dyadmax  23412  ellimc3  23688  dvlip2  23803  dvne0  23819  zabsle1  25066  2lgslem3  25174  axcontlem4  25892  umgrislfupgrlem  26062  uhgr2edg  26145  ushgredgedg  26166  ushgredgedgloop  26168  nb3grprlem1  26326  rusgr1vtx  26540  wlkv0  26603  wlkonl1iedg  26617  uhgrwkspthlem2  26706  usgr2wlkneq  26708  usgr2trlncl  26712  uspgrn2crct  26756  wspthsnonn0vne  26882  umgrwwlks2on  26923  elwspths2on  26926  erclwwlktr  26979  erclwwlkntr  27035  frgrnbnb  27273  frgr2wwlk1  27309  frrusgrord  27321  2clwwlk2clwwlklem2  27330  frgrregord013  27382  isch3  28226  ocin  28283  shmodsi  28376  spansneleq  28557  stj  29222  atom1d  29340  atcvat2i  29374  chirredlem1  29377  chirredi  29381  mdsymlem3  29392  mdsymlem6  29395  bnj849  31121  pconnconn  31339  cvmsss2  31382  cvmliftlem7  31399  mclsind  31593  dfpo2  31771  dfon2lem9  31820  dfon2  31821  frr3g  31904  scutun12  32042  cgrextend  32240  btwntriv2  32244  btwncomim  32245  btwnexch3  32252  funtransport  32263  ifscgr  32276  colinearxfr  32307  lineext  32308  fscgr  32312  outsideoftr  32361  trer  32435  finminlem  32437  fnessref  32477  fgmin  32490  bj-andnotim  32698  bj-alanim  32721  bj-0int  33180  relowlssretop  33341  finxpsuclem  33364  wl-ax13lem1  33417  poimirlem29  33568  itg2addnclem3  33593  itg2addnc  33594  areacirc  33635  ismtybndlem  33735  heibor1lem  33738  iss2  34252  prtlem17  34480  riotasvd  34560  lshpsmreu  34714  atnle  34922  cvratlem  35025  cvrat2  35033  3dim1  35071  2llnjN  35171  2lplnj  35224  linepsubN  35356  pmapsub  35372  paddasslem14  35437  pclfinN  35504  ispsubcl2N  35551  pclfinclN  35554  ldilval  35717  trlord  36174  cdlemk36  36518  dihlsscpre  36840  baerlem3lem2  37316  baerlem5alem2  37317  baerlem5blem2  37318  pellexlem5  37714  pellex  37716  pell1234qrmulcl  37736  pellfundex  37767  relexpmulnn  38318  clsk1indlem3  38658  19.41rg  39083  iunconnlem2  39485  nltle2tri  41648  iccpartnel  41699  fmtnofac2lem  41805  sfprmdvdsmersenne  41845  lighneallem3  41849  lighneallem4  41852  bgoldbtbnd  42022  upgrwlkupwlk  42046  nzerooringczr  42397  ldepspr  42587  aacllem  42875
  Copyright terms: Public domain W3C validator