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

Theorem 3expa 1256
Description: Exportation from triple to double conjunction. (Contributed by NM, 20-Aug-1995.)
Hypothesis
Ref Expression
3exp.1 ((𝜑𝜓𝜒) → 𝜃)
Assertion
Ref Expression
3expa (((𝜑𝜓) ∧ 𝜒) → 𝜃)

Proof of Theorem 3expa
StepHypRef Expression
1 3exp.1 . . 3 ((𝜑𝜓𝜒) → 𝜃)
213exp 1255 . 2 (𝜑 → (𝜓 → (𝜒𝜃)))
32imp31 446 1 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382  w3a 1030
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  df-3an 1032
This theorem is referenced by:  3anidm23  1376  mp3an2  1403  mpd3an3  1416  rgen3  2958  moi2  3353  sbc3ie  3473  2if2  4085  preq12bg  4321  prel12g  4322  ralxfrd2  4805  reuhypd  4816  otsndisj  4895  funcnvqp  5852  fvtp1g  6346  fntpb  6356  f1imass  6400  weisoeq  6483  f1ofveu  6522  f1ocnvfv3  6523  curry1f  7135  curry2f  7137  funsssuppss  7185  tfrlem11  7348  oalimcl  7504  oeordsuc  7538  oelim2  7539  nneob  7596  mapxpen  7988  findcard  8061  wemaplem3  8313  en2eqpr  8690  infxpabs  8894  infxp  8897  cfflb  8941  cfsmolem  8952  isf32lem12  9046  fin1a2lem9  9090  fin1a2s  9096  axcc3  9120  axdc3lem4  9135  zornn0g  9187  pwfseqlem4  9340  tskwun  9462  tskint  9463  tskxp  9465  tskmap  9466  gruf  9489  gruwun  9491  grutsk1  9499  addcanpi  9577  ltapi  9581  mul4  10056  add4  10107  2addsub  10146  addsubeq4  10147  muladd  10313  ltleadd  10360  receu  10521  p1le  10715  lemul12b  10729  lbinf  10825  zdiv  11279  fzind  11307  fnn0ind  11308  uzss  11540  zbtwnre  11618  qmulcl  11638  qreccl  11640  xrlttr  11808  xaddass  11908  xmulasslem3  11945  xmulass  11946  xadddilem  11953  xrsupsslem  11965  xrinfmsslem  11966  supxrunb1  11977  ixxin  12019  ioo0  12027  ico0  12048  ioc0  12049  icc0  12050  iooshf  12079  prunioo  12128  ioojoin  12130  elfz5  12160  elfz0fzfz0  12268  elfzonelfzo  12391  fzind2  12403  mulexpz  12717  expsub  12725  digit2  12814  digit1  12815  facndiv  12892  faclbnd4lem4  12900  faclbnd4  12901  faclbnd5  12902  bccmpl  12913  bcval5  12922  bcpasc  12925  hashunx  12988  ccatrn  13171  swrdccat1  13255  swrdccat2  13256  swrdswrd  13258  cats1un  13273  cshf1  13353  crim  13649  absmax  13863  ello12r  14042  elo12r  14053  climshftlem  14099  2sumeq2dv  14229  expcnv  14381  2cprodeq2dv  14440  rpnnen2lem7  14734  dvdsval3  14771  dvdsnegb  14783  muldvds1  14790  muldvds2  14791  dvdscmul  14792  dvdsmulc  14793  dvdsmulcr  14795  dvds2ln  14798  divalgb  14911  ndvdssub  14917  gcddiv  15052  lcmfval  15118  lcmfcl  15125  dvdslcmf  15128  rpexp1i  15217  phiprmpw  15265  hashgcdeq  15278  pythagtriplem1  15305  pockthg  15394  infpnlem1  15398  4sqlem3  15438  0ramcl  15511  firest  15862  imasaddfnlem  15957  imasleval  15970  xpsfrn2  15999  mrerintcl  16026  iscatd  16103  fullestrcsetc  16560  fullsetcestrc  16575  clatleglb  16895  mreclatBAD  16956  pslem  16975  mrcmndind  17135  grplmulf1o  17258  grplactcnv  17287  mulgnn0subcl  17323  mulgsubcl  17324  mulgdir  17342  issubg2  17378  issubgrpd2  17379  cycsubgcl  17389  cycsubgss  17390  nmzsubg  17404  eqgen  17416  ghmmulg  17441  conjghm  17460  symgfixfo  17628  odeq  17738  odval2  17739  odf1  17748  dfod2  17750  gexdvds  17768  gexdvds2  17769  gexcl2  17773  gexdvds3  17774  sylow2blem2  17805  efgsp1  17919  efgrelexlemb  17932  mulgmhm  18002  mulgghm  18003  iscyggen2  18052  iscyg3  18057  srglmhm  18304  srgrmhm  18305  ringlghm  18373  ringrghm  18374  gsumdixp  18378  dvdsrcl2  18419  crngunit  18431  kerf1hrm  18512  subrgugrp  18568  cntzsubr  18581  lmodvsdir  18656  lmodvsass  18657  lmodvsghm  18693  lsssubg  18724  lss1d  18730  islbs2  18921  lidlsubg  18982  lidlsubcl  18983  quscrng  19007  lpigen  19023  xrsdsreval  19556  expghm  19608  mulgghm2  19609  ip0r  19746  obs2ss  19834  islindf3  19926  scmatscm  20080  scmataddcl  20083  scmatsubcl  20084  scmatfo  20097  matunit  20245  cpmatelimp  20278  cpmatelimp2  20280  cpmatinvcl  20283  cpmatmcl  20285  mat2pmatf  20294  m2cpmf  20308  cpm2mf  20318  m2cpmfo  20322  m2cpminv  20326  decpmataa0  20334  pm2mpf  20364  pm2mpf1  20365  idpm2idmp  20367  pm2mpfo  20380  elcls2  20630  opnnei  20676  innei  20681  iscnp4  20819  cnpnei  20820  iscncl  20825  cnnei  20838  cnconst  20840  ordthauslem  20939  bwth  20965  1stccnp  21017  llyrest  21040  nllyrest  21041  kgenss  21098  xkoccn  21174  kqsat  21286  kqt0lem  21291  isr0  21292  fbssfi  21393  isfild  21414  filcon  21439  trfilss  21445  fgtr  21446  ufileu  21475  ufilen  21486  fmfnfmlem4  21513  fmfnfm  21514  hausflimi  21536  cnpflf2  21556  cnpflf  21557  cnflf  21558  cnpfcf  21597  cnfcf  21598  cnextcn  21623  tmdmulg  21648  clsnsg  21665  tsmsxplem1  21708  tsmsxp  21710  ustuqtop0  21796  ismeti  21881  isxmet2d  21883  elbl2ps  21945  elbl2  21946  xblpnfps  21951  xblpnf  21952  xbln0  21970  blin  21977  blssexps  21982  blssex  21983  blsscls2  22060  blcls  22062  blsscls  22063  metss  22064  metrest  22080  metcn  22099  metustbl  22122  psmetutop  22123  nmf2  22148  ngpi  22182  nmdvr  22217  nmoi  22274  nmoix  22275  nmoleub  22277  nghmcn  22291  xrsxmet  22352  iccntr  22364  metdsle  22394  icoopnst  22477  iocopnst  22478  icccvx  22488  pi1xfr  22594  isclmi0  22637  iscvsi  22666  lmmbr  22782  lmmbr2  22783  iscfil3  22797  iscau2  22801  cfilres  22820  bcthlem1  22846  bcthlem4  22849  bcthlem5  22850  rrxmet  22916  ioombl  23057  iccvolcl  23059  ioovolcl  23061  mbfi1fseqlem3  23207  mbfi1fseqlem4  23208  mbfi1fseqlem5  23209  ig1pcl  23656  ig1prsp  23658  aannenlem1  23804  taylplem1  23838  dvtaylp  23845  relogeftb  24052  logdivlt  24088  cxpexp  24131  rpcxpcl  24139  isppw2  24558  vmappw  24559  lgslem4  24742  lgscllem  24746  lgsneg1  24764  lgsne0  24777  cgraswap  25430  brbtwn2  25503  ax5seglem1  25526  ax5seglem2  25527  axcontlem4  25565  nbgraf1olem5  25740  constr3cycl  25955  wwlknimp  25981  usg2wlkeq  26002  wwlknred  26017  wwlknext  26018  clwwlknprop  26066  3cyclfrgrarn1  26305  3cyclfrgrarn  26306  4cycl2vnunb  26310  frgrancvvdeqlemB  26331  usgreghash2spotv  26359  2spotmdisj  26361  grpoidinvlem3  26510  isvciOLD  26603  nmcvcn  26735  ipval2lem2  26744  ipval2lem5  26750  sspival  26781  sspimsval  26783  isblo2  26828  nmoo0  26836  blocni  26850  isph  26867  sspph  26900  hvadd4  27083  hiassdi  27138  ocsh  27332  chj4  27584  spansncol  27617  pjjsi  27749  hoscl  27794  hodcl  27796  hoadd4  27833  homco1  27850  homulass  27851  hoadddi  27852  hoadddir  27853  unoplin  27969  adjvalval  27986  hmoplin  27991  bralnfn  27997  brafnmul  28000  lnopmi  28049  lnopcoi  28052  hmops  28069  hmopm  28070  nmophmi  28080  lnfncnbd  28106  cnlnadjlem2  28117  adjlnop  28135  adjmul  28141  adjadd  28142  branmfn  28154  kbass5  28169  kbass6  28170  leop2  28173  leopadd  28181  leopmuli  28182  pjimai  28225  atcvatlem  28434  chirredlem2  28440  mdsymlem3  28454  mdsymlem5  28456  sumdmdii  28464  sumdmdlem  28467  cdj3lem2a  28485  cdj3lem2b  28486  cdj3lem3a  28488  cdj3i  28490  xreceu  28767  toslublem  28804  tosglblem  28806  ogrpaddltbi  28856  archiabllem1b  28883  archiabllem2c  28886  archiabl  28889  slmdvsdir  28906  slmdvsass  28907  pstmxmet  29074  ordtconlem1  29104  hasheuni  29280  omsf  29491  ballotlemirc  29726  signswmnd  29766  bnj1204  30140  txpcon  30274  cvmscld  30315  elmpps  30530  dfrdg2  30751  wsuclem  30823  wsuclemOLD  30824  nobndlem8  30904  segconeu  31094  linecom  31233  linethru  31236  lineintmo  31240  fnemeet2  31338  fnejoin2  31340  lindsdom  32369  lindsenlbs  32370  matunitlindflem1  32371  matunitlindflem2  32372  heicant  32410  mblfinlem1  32412  mblfinlem3  32414  ismblfin  32416  cnambfre  32424  itg2addnclem2  32428  ftc1anclem1  32451  ftc1anclem5  32455  ftc1anclem6  32456  ftc2nc  32460  areacirclem2  32467  areacirclem4  32469  areacirclem5  32470  areacirc  32471  fzmul  32503  subspopn  32514  isbndx  32547  isbnd2  32548  isbnd3  32549  ssbnd  32553  prdstotbnd  32559  heibor1  32575  rrnmet  32594  rngonegmn1l  32706  rngohomco  32739  rngoisocnv  32746  rngoisoco  32747  crngohomfo  32771  isidlc  32780  rngoidl  32789  prnc  32832  ispridlc  32835  cvrval2  33375  glbconxN  33478  hlrelat5N  33501  cvratlem  33521  cvrat2  33529  athgt  33556  3dim2  33568  llnn0  33616  lplnn0N  33647  lvoln0N  33691  snatpsubN  33850  paddasslem18  33937  pmod1i  33948  lhpexle2  34110  lhpexle3lem  34111  lhpexle3  34112  ldilcnv  34215  trlcnv  34266  trlnidatb  34278  cdleme32snaw  34537  cdleme32fvaw  34541  cdleme42ke  34587  cdlemeg46gf  34635  cdleme50trn12  34654  cdlemg1cex  34690  cdlemb3  34708  tgrpgrplem  34851  tgrpabl  34853  tendoplcl2  34880  tendo0pl  34893  tendoicl  34898  tendoipl  34899  cdlemkid3N  35035  tendoex  35077  erngdvlem4  35093  erngdvlem4-rN  35101  dib1dim  35268  dib1dim2  35271  dihglbcpreN  35403  dihmeetALTN  35430  dih1dimatlem  35432  dihatlat  35437  oddcomabszz  36323  acongtr  36359  rpnnen3lem  36412  islssfg  36454  lmhmfgsplit  36470  unxpwdom3  36479  hbtlem7  36510  sdrgacs  36586  iocmbl  36613  ss2iundf  36766  nzss  37334  dvconstbi  37351  bccbc  37362  uzmptshftfval  37363  iccdifprioo  38386  dvnmul  38630  volico  38673  volioore  38680  fourierdlem74  38870  fourierdlem75  38871  issald  39024  sge0iunmptlemfi  39103  sge0iunmptlemre  39105  sge0iunmpt  39108  sge0xp  39119  hspmbllem2  39314  smflimlem3  39456  nnsum4primesodd  40010  nnsum4primesoddALTV  40011  pfxccat1  40071  ewlkprop  40800  uspgr2wlkeq  40849  uhgr1wlkspthlem2  40955  eupth2lem3lem7  41397  frgr3vlem2  41439  3cyclfrgrrn1  41450  4cycl2vnunb-av  41455  frgrncvvdeqlemB  41472  rnghmsubcsetclem2  41763  rhmsubcsetclem2  41809  rhmsubcrngclem2  41815  lcoss  42014  snlindsntorlem  42048  aacllem  42312
  Copyright terms: Public domain W3C validator