NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  expcom Unicode version

Theorem expcom 424
Description: Exportation inference with commuted antecedents. (Contributed by NM, 25-May-2005.)
Hypothesis
Ref Expression
exp.1
Assertion
Ref Expression
expcom

Proof of Theorem expcom
StepHypRef Expression
1 exp.1 . . 3
21ex 423 . 2
32com12 27 1
Colors of variables: wff setvar class
Syntax hints:   wi 4   wa 358
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 177  df-an 360
This theorem is referenced by:  ancoms  439  syldan  456  sylan  457  4casesdan  916  dedlema  920  dedlemb  921  dvelimv  1939  cbval2  2004  cbvex2  2005  2moswap  2279  2mos  2283  2eu2  2285  pm2.61ne  2591  r19.21be  2715  uneqdifeq  3638  ssunsn2  3865  ssuni  3913  uniss2  3922  elpwuni  4053  lenltfin  4469  tfincl  4492  tfinltfin  4501  evenoddnnnul  4514  nnadjoin  4520  vfinncvntnn  4548  fun  5236  tz6.12c  5347  eqfnfv  5392  fnressn  5438  fressnfv  5439  fconst2g  5452  eloprabga  5578  ndmovcl  5614  fvmptnf  5723  mapsn  6026  mapss  6027  enprmaplem3  6078  sbthlem2  6204  nmembers1lem3  6270  nchoicelem12  6300
  Copyright terms: Public domain W3C validator