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

Theorem impancom 456
Description: Mixed importation/commutation inference. (Contributed by NM, 22-Jun-2013.)
Hypothesis
Ref Expression
impancom.1 ((𝜑𝜓) → (𝜒𝜃))
Assertion
Ref Expression
impancom ((𝜑𝜒) → (𝜓𝜃))

Proof of Theorem impancom
StepHypRef Expression
1 impancom.1 . . . 4 ((𝜑𝜓) → (𝜒𝜃))
21ex 450 . . 3 (𝜑 → (𝜓 → (𝜒𝜃)))
32com23 86 . 2 (𝜑 → (𝜒 → (𝜓𝜃)))
43imp 445 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:  eqrdav  2620  rexraleqim  3312  disjiun  4603  propeqop  4930  euotd  4935  pwssun  4980  funopsn  6367  isotr  6540  el2mpt2csbcl  7195  ressuppssdif  7261  oeordi  7612  domunsncan  8004  pssnn  8122  findcard3  8147  ordtypelem7  8373  inf3lem5  8473  r1tr  8583  cardmin2  8768  ac10ct  8801  isf32lem12  9130  isfin1-3  9152  fin17  9160  fin1a2s  9180  axdc4lem  9221  axcclem  9223  ttukeylem2  9276  genpcd  9772  ltexprlem3  9804  prlem936  9813  supsrlem  9876  mul0or  10611  fiminre  10916  un0addcl  11270  un0mulcl  11271  btwnnz  11397  uznfz  12364  elfz0ubfz0  12384  elfzo0z  12450  fzofzim  12455  elfzom1p1elfzo  12488  ssfzoulel  12503  ssfzo12bi  12504  subfzo0  12530  modmuladdim  12653  modaddmodup  12673  modfzo0difsn  12682  axdc4uzlem  12722  expaddz  12844  sq01  12926  hashnn0n0nn  13120  hashss  13137  hashgt12el  13150  fi1uzind  13218  brfi1indALT  13221  fi1uzindOLD  13224  brfi1indALTOLD  13227  ccatalpha  13314  swrdswrdlem  13397  swrdswrd  13398  swrdccatin1  13420  swrdccatin12lem3  13427  repswswrd  13468  cshwmodn  13478  cshf1  13493  cshw1  13505  2cshwcshw  13508  sqrmo  13926  caubnd2  14031  summo  14381  nno  15022  divalglem8  15047  lcmdvds  15245  lcmfunsnlem1  15274  hashgcdeq  15418  modprm0  15434  pcqcl  15485  vdwnnlem3  15625  prmgaplem5  15683  prmgaplem7  15685  catpropd  16290  cicsym  16385  isinitoi  16574  istermoi  16575  iszeroi  16580  acsfiindd  17098  tsrlemax  17141  issubg4  17534  gsmsymgreqlem2  17772  oddvdsnn0  17884  oddvds  17887  gexdvds  17920  lt6abl  18217  pgpfac1lem3  18397  coe1ae0  19505  isphld  19918  mdetdiaglem  20323  slesolex  20407  pmatcoe1fsupp  20425  cpmatelimp  20436  cpmatelimp2  20438  cpmatmcllem  20442  pm2mpf1  20523  mp2pm2mplem4  20533  fvmptnn04ifa  20574  fvmptnn04ifd  20577  chfacfscmul0  20582  chfacfpmmul0  20586  neii1  20820  neii2  20822  uncmp  21116  isfild  21572  fbunfip  21583  fgss2  21588  fgcl  21592  isufil2  21622  cfinufil  21642  ufilen  21644  fsumcn  22581  lmmbr  22964  iscau4  22985  caussi  23003  ovoliunnul  23182  ovolicc2lem4  23195  itg1ge0a  23384  rolle  23657  ulmcaulem  24052  cxpge0  24329  fsumvma  24838  gausslemma2dlem1a  24990  2sqb  25057  pntrsumbnd2  25156  pntlem3  25198  axeuclid  25743  axcontlem2  25745  usgrislfuspgr  25972  nbuhgr2vtx1edgblem  26134  usgredgsscusgredg  26242  upgrwlkvtxedg  26410  uspgr2wlkeq  26411  cyclnspth  26564  uspgrn2crct  26569  crctcshwlkn0lem4  26574  wlkiswwlks2lem5  26628  wlknewwlksn  26642  wlkwwlksur  26652  umgrwwlks2on  26719  clwlkclwwlklem2a4  26765  clwlkclwwlklem2a  26766  clwwlksel  26780  wwlksubclwwlks  26791  clwwisshclwwslemlem  26792  clwlksfoclwwlk  26829  uhgr3cyclexlem  26907  vdgn1frgrv3  27025  frgrncvvdeqlem3  27029  frgrncvvdeqlem4  27030  numclwwlkovf2ex  27075  frgrregord013  27107  spansncvi  28360  lnconi  28741  cdj3lem1  29142  spc2ed  29161  metider  29719  nofv  31511  sltres  31518  finminlem  31954  clsint2  31966  bj-finsumval0  32780  finxpsuclem  32866  wl-exeq  32953  phpreu  33025  poimirlem26  33067  poimir  33074  ismtyima  33234  elpaddn0  34566  tendospcanN  35792  rexzrexnn0  36848  unxpwdom3  37145  fsovrfovd  37785  radcnvrat  37995  zm1nn  40613  subsubelfzo0  40633  fzoopth  40634  2ffzoeq  40635  fargshiftf  40674  2pwp1prm  40802  lighneal  40827  isassintop  41134  uzlidlring  41217  2zrngamgm  41227  ply1mulgsumlem1  41462  suppdm  41588
  Copyright terms: Public domain W3C validator