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

Theorem 3exp 1141
Description: Exportation inference. (Contributed by NM, 30-May-1994.) (Proof shortened by Wolf Lammen, 22-Jun-2022.)
Hypothesis
Ref Expression
3exp.1 ((𝜑𝜓𝜒) → 𝜃)
Assertion
Ref Expression
3exp (𝜑 → (𝜓 → (𝜒𝜃)))

Proof of Theorem 3exp
StepHypRef Expression
1 3exp.1 . . 3 ((𝜑𝜓𝜒) → 𝜃)
213expa 1140 . 2 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
32exp31 408 1 (𝜑 → (𝜓 → (𝜒𝜃)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1100
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 198  df-an 385  df-3an 1102
This theorem is referenced by:  3expb  1142  3expiaOLD  1144  3expib  1145  3com12  1146  3com13  1147  syl3an2OLD  1197  syl3an3OLD  1199  ad4ant123OLD  1207  ad4ant124OLD  1209  ad4ant134OLD  1211  ad4ant234OLD  1213  pm3.2an3  1432  3expaOLD  1439  3com23OLD  1442  3imp3i2anOLD  1446  3an1rsOLD  1447  3exp1  1454  3expd  1455  exp5o  1457  ad5ant245OLD  1464  ad5ant234OLD  1466  ad5ant235OLD  1468  ad5ant123OLD  1470  ad5ant124OLD  1472  ad5ant125OLD  1474  ad5ant134OLD  1476  ad5ant135OLD  1478  ad5ant145OLD  1480  syl2an23anOLD  1540  3ecase  1591  rexlimdv3a  3221  rabssdv  3879  reupick2  4114  disjiund  4835  otiunsndisj  5175  wefrc  5305  predpo  5911  tz7.7  5962  unizlim  6057  fveqdmss  6576  f1oiso2  6826  ssorduni  7215  suceloni  7243  tfisi  7288  poxp  7523  smo11  7697  tfrlem5  7712  odi  7896  omass  7897  nndi  7940  nnmass  7941  mapsnd  8134  undifixp  8181  findcard  8438  ac6sfi  8443  domunfican  8472  mapfien2  8553  fisup2g  8613  fiinf2g  8645  indcardi  9147  acndom  9157  ackbij1lem16  9342  infpssrlem4  9413  fin23lem11  9424  isfin2-2  9426  fin23lem34  9453  fin1a2lem10  9516  hsmexlem2  9534  axcc3  9545  domtriomlem  9549  axdc3lem2  9558  axdc3lem4  9560  axcclem  9564  ttukeyg  9624  axdclem2  9627  axacndlem4  9717  axacndlem5  9718  axacnd  9719  tskr1om2  9875  tskwe2  9880  tskord  9887  tskcard  9888  tskuni  9890  tskwun  9891  gruiin  9917  grudomon  9924  gruina  9925  mulcanpi  10007  adderpq  10063  mulerpq  10064  dedekindle  10486  divgt0  11176  divge0  11177  uzind  11735  uzind2  11736  iccsplit  12528  ssnn0fi  13008  sqlecan  13194  modexp  13222  facavg  13308  2cshwcshw  13795  relexpcnv  13998  relexpreld  14003  relexpaddnn  14014  relexpaddg  14016  prodfn0  14847  prodfrec  14848  ntrivcvgfvn0  14852  fprodabs  14925  fprodle  14947  bpolycl  15003  bpolydif  15006  fprodefsum  15045  dvdsmodexp  15211  dvdsaddre2b  15252  dvdsnprmd  15621  prmndvdsfaclt  15652  ncoprmlnprm  15653  fermltl  15706  pceu  15768  setsstruct2  16107  setsstruct  16109  mreexexd  16513  initoeu1  16865  termoeu1  16872  isglbd  17322  mulgaddcom  17768  pmtrfrn  18079  psgnunilem4  18118  mulgass2  18803  islss4  19169  lspsneu  19330  lspfixed  19335  lspfixedOLD  19336  lspexch  19337  lsmcv  19349  lspsolvlem  19350  xrsdsreclblem  20000  isphld  20209  mdetralt  20625  mdetunilem9  20637  fiinopn  20919  neips  21131  tpnei  21139  neindisj2  21141  opnneiid  21144  hausnei2  21371  cmpsublem  21416  cmpsub  21417  cmpcld  21419  comppfsc  21549  filufint  21937  cfinufil  21945  rnelfm  21970  alexsubALTlem1  22064  alexsubALTlem4  22067  alexsubALT  22068  tsmsxp  22171  neibl  22519  tngngp3  22673  tgqioo  22816  ovolunlem2  23479  iunmbl2  23538  itg1le  23694  vieta1  24281  aannenlem2  24298  aalioulem3  24303  aalioulem4  24304  aaliou2  24309  wilthlem3  25010  bcmono  25216  gausslemma2dlem1a  25304  axcontlem7  26064  edglnl  26253  numedglnl  26254  ausgrumgri  26277  ausgrusgri  26278  usgrausgrb  26279  usgredg2vtxeuALT  26329  ushgredgedg  26336  ushgredgedgloop  26338  ushgredgedgloopOLD  26339  nbuhgr2vtx1edgb  26464  cusgrsize2inds  26577  upgrewlkle2  26730  wlkl1loop  26762  redwlk  26797  pthdivtx  26853  pthdadjvtx  26854  upgr2pthnlp  26856  upgrspthswlk  26862  clwlkl1loop  26907  wwlksnred  27029  wwlksnextbi  27031  elwwlks2ons3im  27094  elwwlks2ons3OLD  27096  umgrwwlks2on  27098  clwwlknwwlksn  27186  clwwlknwwlksnOLD  27187  clwwlkinwwlk  27189  wwlksext2clwwlk  27207  clwlksfclwwlkOLD  27236  1pthon2v  27326  uhgr3cyclex  27355  n4cyclfrgr  27466  frgrwopreg  27498  numclwwlk1lem2f1  27536  clwwlknonclwlknonf1o  27542  wlkl0  27547  frgrreggt1  27581  frgrreg  27582  frgrregord013  27583  chintcli  28518  spansnss  28758  elspansn4  28760  chscllem4  28827  hoadddir  28991  adjmul  29279  kbass6  29308  spansncv2  29480  sumdmdii  29602  nexple  30396  bnj1417  31432  mclsind  31790  iprodefisumlem  31948  poseq  32074  btwndiff  32455  elicc3  32632  finminlem  32633  sdclem2  33849  clmgmOLD  33961  grpomndo  33985  zerdivemp1x  34057  lsmsat  34788  lsmcv2  34809  lcvat  34810  lsatcveq0  34812  lcvexchlem4  34817  lcvexchlem5  34818  islshpcv  34833  l1cvpat  34834  lshpkrlem6  34895  omlfh3N  35039  cvlsupr4  35125  cvlsupr5  35126  cvlsupr6  35127  2llnneN  35189  hlrelat3  35192  cvrval3  35193  cvrval4N  35194  cvrexchlem  35199  2atlt  35219  cvrat4  35223  atbtwnexOLDN  35227  atbtwnex  35228  athgt  35236  3dim1  35247  3dim2  35248  3dim3  35249  1cvratex  35253  llnle  35298  atcvrlln2  35299  atcvrlln  35300  2llnmat  35304  lplnle  35320  lplnnle2at  35321  lplnnlelln  35323  llncvrlpln2  35337  2llnjN  35347  lvoli2  35361  lvolnlelln  35364  lvolnlelpln  35365  4atlem10  35386  4atlem11  35389  4atlem12  35392  lplncvrlvol2  35395  2lplnj  35400  lneq2at  35558  lnatexN  35559  lnjatN  35560  lncvrat  35562  2lnat  35564  cdlemb  35574  paddasslem14  35613  llnexchb2  35649  dalawlem10  35660  dalawlem13  35663  dalawlem14  35664  dalaw  35666  pclclN  35671  pclfinN  35680  osumcllem11N  35746  lhp2lt  35781  lhpexle3lem  35791  4atexlem7  35855  ldilcnv  35895  ldilco  35896  ltrncnv  35926  trlval2  35944  cdleme24  36133  cdleme26ee  36141  cdleme28  36154  cdleme32le  36228  cdleme50trn2  36332  cdleme50ltrn  36338  cdleme  36341  cdlemf1  36342  cdlemf  36344  cdlemg1cex  36369  cdlemg2ce  36373  cdlemg18b  36460  ltrnco  36500  tendocan  36605  cdlemk28-3  36689  cdlemk11t  36727  dia2dimlem6  36850  dia2dimlem12  36856  dihlsscpre  37015  dihord4  37039  dihord5b  37040  dihmeetlem3N  37086  dihmeetlem20N  37107  dvh4dimlem  37224  lclkrlem2y  37312  mapdpglem24  37485  mapdpglem32  37486  mapdpg  37487  baerlem3lem2  37491  baerlem5alem2  37492  baerlem5blem2  37493  mapdh9a  37570  mapdh9aOLDN  37571  hdmap14lem6  37654  hdmapglem7  37710  mzpexpmpt  37810  pellexlem5  37899  pellex  37901  pell14qrexpclnn0  37932  pellfundex  37952  monotuz  38007  monotoddzzfi  38008  expmordi  38013  rmxypos  38015  jm2.17a  38028  jm2.17b  38029  rmygeid  38032  jm2.19lem3  38059  jm2.15nn0  38071  jm2.16nn0  38072  aomclem2  38126  aomclem6  38130  dfac11  38133  hbtlem5  38199  cnsrexpcl  38236  relexpxpnnidm  38495  relexpiidm  38496  relexpss1d  38497  iunrelexpmin1  38500  relexpmulnn  38501  iunrelexpmin2  38504  relexp01min  38505  relexp0a  38508  relexpxpmin  38509  relexpaddss  38510  trclimalb2  38518  3impexpbicomi  39184  ee333  39211  eel12131  39436  eel2122old  39441  e333  39457  ordelordALTVD  39597  refsumcn  39683  uzwo4  39714  ssinc  39757  ssdec  39758  iunincfi  39765  restuni3  39793  eliuniin2  39795  rabssd  39822  reximdd  39833  suprnmpt  39844  wessf1ornlem  39860  disjf1o  39867  fompt  39868  disjinfi  39869  ssnnf1octb  39871  choicefi  39879  mapssbi  39892  unirnmapsn  39893  ssmapsn  39895  iunmapsn  39896  funimassd  39915  rnmptlb  39937  rnmptbddlem  39939  fvelimad  39942  infnsuprnmpt  39948  fperiodmullem  39998  upbdrech  40000  ssfiunibd  40004  supxrgere  40029  iuneqfzuzlem  40030  supxrgelem  40033  supxrge  40034  suplesup  40035  infrpge  40047  infleinf  40068  suplesup2  40072  supxrunb3  40102  infleinf2  40120  rexabslelem  40124  infrnmptle  40129  infxrunb3rnmpt  40134  iccshift  40225  iooshift  40229  fmul01  40292  fmuldfeq  40295  fmul01lt1  40298  mullimc  40328  islptre  40331  mullimcf  40335  limcperiod  40340  islpcn  40351  limsupre  40353  limcleqr  40356  neglimc  40359  addlimc  40360  0ellimcdiv  40361  limclner  40363  fnlimfvre  40386  limsuppnflem  40422  limsupmnfuzlem  40438  limsupre3lem  40444  limsupre3uzlem  40447  climuzlem  40455  limsupgtlem  40489  coskpi2  40557  cosknegpi  40560  cncfshift  40567  cncfperiod  40572  icccncfext  40580  dvnmptdivc  40633  dvnmptconst  40636  dvnmul  40638  dvmptfprodlem  40639  dvmptfprod  40640  dvnprodlem1  40641  dvnprodlem2  40642  iblspltprt  40668  itgspltprt  40674  itgperiod  40676  ismbl3  40682  stoweidlem3  40699  stoweidlem31  40727  stoweidlem59  40755  stirlinglem13  40782  fourierdlem41  40844  fourierdlem42  40845  fourierdlem48  40850  fourierdlem51  40853  fourierdlem53  40855  fourierdlem70  40872  fourierdlem71  40873  fourierdlem73  40875  fourierdlem80  40882  fourierdlem81  40883  fourierdlem89  40891  fourierdlem91  40893  fourierdlem93  40895  fourierdlem97  40899  elaa2  40930  qndenserrnopnlem  40996  salexct  41031  subsaliuncl  41055  subsalsal  41056  sge0tsms  41076  sge0f1o  41078  sge0fsum  41083  sge0supre  41085  sge0sup  41087  sge0rnbnd  41089  sge0gerp  41091  sge0pnffigt  41092  sge0lefi  41094  sge0ltfirp  41096  sge0resrn  41100  sge0resplit  41102  sge0split  41105  sge0iunmptlemfi  41109  sge0iunmptlemre  41111  sge0iunmpt  41114  sge0rpcpnf  41117  sge0isum  41123  sge0xp  41125  sge0xaddlem2  41130  sge0uzfsumgt  41140  sge0seq  41142  sge0reuz  41143  nnfoctbdjlem  41151  nnfoctbdj  41152  iundjiun  41156  meadjiunlem  41161  voliunsge0lem  41168  meaiuninclem  41176  meaiininc2  41184  carageniuncllem1  41217  carageniuncllem2  41218  caratheodorylem1  41222  caratheodorylem2  41223  isomenndlem  41226  ovnsupge0  41253  ovnlerp  41258  ovncvrrp  41260  ovnsubaddlem1  41266  hoidmvval0  41283  hoidmv1lelem3  41289  hoidmv1le  41290  hoidmvlelem1  41291  hoidmvlelem2  41292  hoidmvlelem3  41293  ovnhoilem2  41298  opnvonmbllem2  41329  ovolval5lem3  41350  ovnovollem3  41354  vonioo  41378  vonicc  41381  pimiooltgt  41403  sssmf  41429  smfaddlem1  41453  smflimlem6  41466  smfmullem4  41483  smfpimbor1lem1  41487  smfco  41491  smfpimcc  41496  smflimmpt  41498  smfinflem  41505  smflimsuplem7  41514  smflimsuplem8  41515  smflimsupmpt  41517  smfliminfmpt  41520  iccpartiltu  41933  goldbachth  42034  fmtnofac1  42057  prmdvdsfmtnof1lem1  42071  pwdif  42076  lighneal  42103  sprsymrelfvlem  42308  uspgropssxp  42320  rngccatidALTV  42557  ringccatidALTV  42620  nzerooringczr  42640  lcosslsp  42795  fllog2  42930  dignn0flhalf  42980  iunord  42990  setrec2fun  43007
  Copyright terms: Public domain W3C validator