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

Theorem 3expa 1284
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 1283 . 2 (𝜑 → (𝜓 → (𝜒𝜃)))
32imp31 447 1 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  w3a 1054
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  df-3an 1056
This theorem is referenced by:  ad4ant123  1319  ad4ant124  1321  ad4ant134  1323  ad4ant234  1329  3anidm23  1425  mp3an2  1452  mpd3an3  1465  rgen3  3005  moi2  3420  sbc3ie  3540  2if2  4169  preq12bg  4417  prel12g  4418  ralxfrd2  4914  reuhypd  4925  otsndisj  5008  funcnvqp  5990  fvtp1g  6504  fntpb  6514  f1imass  6561  weisoeq  6645  f1ofveu  6685  f1ocnvfv3  6686  curry1f  7316  curry2f  7318  funsssuppss  7366  tfrlem11  7529  oalimcl  7685  oeordsuc  7719  oelim2  7720  nneob  7777  mapxpen  8167  findcard  8240  wemaplem3  8494  en2eqpr  8868  infxpabs  9072  infxp  9075  cfflb  9119  cfsmolem  9130  isf32lem12  9224  fin1a2lem9  9268  fin1a2s  9274  axcc3  9298  axdc3lem4  9313  zornn0g  9365  pwfseqlem4  9522  tskwun  9644  tskint  9645  tskxp  9647  tskmap  9648  gruf  9671  gruwun  9673  grutsk1  9681  addcanpi  9759  ltapi  9763  mul4  10243  add4  10294  2addsub  10333  addsubeq4  10334  muladd  10500  ltleadd  10549  receu  10710  p1le  10904  lemul12b  10918  lbinf  11014  zdiv  11485  fzind  11513  fnn0ind  11514  uzss  11746  zbtwnre  11824  qmulcl  11844  qreccl  11846  xrlttr  12011  xaddass  12117  xmulasslem3  12154  xmulass  12155  xadddilem  12162  xrsupsslem  12175  xrinfmsslem  12176  supxrunb1  12187  ixxin  12230  ioo0  12238  ico0  12259  ioc0  12260  icc0  12261  iooshf  12290  prunioo  12339  ioojoin  12341  elfz5  12372  elfz0fzfz0  12483  elfzonelfzo  12610  fzind2  12626  mulexpz  12940  expsub  12948  digit2  13037  digit1  13038  facndiv  13115  faclbnd4lem4  13123  faclbnd4  13124  faclbnd5  13125  bccmpl  13136  bcval5  13145  bcpasc  13148  hashunx  13213  hashdmpropge2  13303  ccatrn  13407  swrdccat1  13503  swrdccat2  13504  swrdswrd  13506  cats1un  13521  cshf1  13602  crim  13899  absmax  14113  ello12r  14292  elo12r  14303  climshftlem  14349  2sumeq2dv  14480  hash2iun  14599  expcnv  14640  2cprodeq2dv  14699  rpnnen2lem7  14993  dvdsval3  15031  dvdsnegb  15046  muldvds1  15053  muldvds2  15054  dvdscmul  15055  dvdsmulc  15056  dvdsmulcr  15058  dvds2ln  15061  divalgb  15174  ndvdssub  15180  gcddiv  15315  lcmfval  15381  lcmfcl  15388  dvdslcmf  15391  rpexp1i  15480  phiprmpw  15528  hashgcdeq  15541  pythagtriplem1  15568  pockthg  15657  infpnlem1  15661  4sqlem3  15701  0ramcl  15774  firest  16140  imasaddfnlem  16235  imasleval  16248  xpsfrn2  16277  mrerintcl  16304  iscatd  16381  fullestrcsetc  16838  fullsetcestrc  16853  clatleglb  17173  mreclatBAD  17234  pslem  17253  mrcmndind  17413  grplmulf1o  17536  grplactcnv  17565  mulgnn0subcl  17601  mulgsubcl  17602  mulgdir  17620  issubg2  17656  issubgrpd2  17657  cycsubgcl  17667  cycsubgss  17668  nmzsubg  17682  eqgen  17694  ghmmulg  17719  conjghm  17738  symgfixfo  17905  odeq  18015  odval2  18016  odf1  18025  dfod2  18027  gexdvds  18045  gexdvds2  18046  gexcl2  18050  gexdvds3  18051  sylow2blem2  18082  efgsp1  18196  efgrelexlemb  18209  mulgmhm  18279  mulgghm  18280  iscyggen2  18329  iscyg3  18334  srglmhm  18581  srgrmhm  18582  ringlghm  18650  ringrghm  18651  gsumdixp  18655  dvdsrcl2  18696  crngunit  18708  kerf1hrm  18791  subrgugrp  18847  cntzsubr  18860  lmodvsdir  18935  lmodvsass  18936  lmodvsghm  18972  lsssubg  19005  lss1d  19011  islbs2  19202  lidlsubg  19263  lidlsubcl  19264  quscrng  19288  lpigen  19304  xrsdsreval  19839  expghm  19892  mulgghm2  19893  ip0r  20030  obs2ss  20121  islindf3  20213  scmatscm  20367  scmataddcl  20370  scmatsubcl  20371  scmatfo  20384  matunit  20532  cpmatelimp  20565  cpmatelimp2  20567  cpmatinvcl  20570  cpmatmcl  20572  mat2pmatf  20581  m2cpmf  20595  cpm2mf  20605  m2cpmfo  20609  m2cpminv  20613  decpmataa0  20621  pm2mpf  20651  pm2mpf1  20652  idpm2idmp  20654  pm2mpfo  20667  elcls2  20926  opnnei  20972  innei  20977  iscnp4  21115  cnpnei  21116  iscncl  21121  cnnei  21134  cnconst  21136  ordthauslem  21235  bwth  21261  1stccnp  21313  llyrest  21336  nllyrest  21337  kgenss  21394  xkoccn  21470  kqsat  21582  kqt0lem  21587  isr0  21588  fbssfi  21688  isfild  21709  filconn  21734  trfilss  21740  fgtr  21741  ufileu  21770  ufilen  21781  fmfnfmlem4  21808  fmfnfm  21809  hausflimi  21831  cnpflf2  21851  cnpflf  21852  cnflf  21853  cnpfcf  21892  cnfcf  21893  cnextcn  21918  tmdmulg  21943  clsnsg  21960  tsmsxplem1  22003  tsmsxp  22005  ustuqtop0  22091  ismeti  22177  isxmet2d  22179  elbl2ps  22241  elbl2  22242  xblpnfps  22247  xblpnf  22248  xbln0  22266  blin  22273  blssexps  22278  blssex  22279  blsscls2  22356  blcls  22358  blsscls  22359  metss  22360  metrest  22376  metcn  22395  metustbl  22418  psmetutop  22419  nmf2  22444  ngpi  22479  tngngp3  22507  nmdvr  22521  nmoi  22579  nmoix  22580  nmoleub  22582  nghmcn  22596  xrsxmet  22659  iccntr  22671  metdsle  22702  icoopnst  22785  iocopnst  22786  icccvx  22796  pi1xfr  22901  isclmi0  22944  iscvsi  22975  cphipval  23088  lmmbr  23102  lmmbr2  23103  iscfil3  23117  iscau2  23121  cfilres  23140  bcthlem1  23167  bcthlem4  23170  bcthlem5  23171  rrxmet  23237  ioombl  23379  iccvolcl  23381  ioovolcl  23384  mbfi1fseqlem3  23529  mbfi1fseqlem4  23530  mbfi1fseqlem5  23531  ig1pcl  23980  ig1prsp  23982  aannenlem1  24128  taylplem1  24162  dvtaylp  24169  relogeftb  24376  logdivlt  24412  cxpexp  24459  rpcxpcl  24467  isppw2  24886  vmappw  24887  lgslem4  25070  lgscllem  25074  lgsneg1  25092  lgsne0  25105  cgraswap  25757  brbtwn2  25830  ax5seglem1  25853  ax5seglem2  25854  axcontlem4  25892  ewlkprop  26555  uspgr2wlkeq  26598  uhgrwkspthlem2  26706  eupth2lem3lem7  27212  frgr3vlem2  27254  3cyclfrgrrn1  27265  4cycl2vnunb  27270  frgrncvvdeqlem8  27286  grpoidinvlem3  27488  isvciOLD  27563  nmcvcn  27678  ipval2lem2  27687  sspimsval  27721  isblo2  27766  nmoo0  27774  blocni  27788  isph  27805  sspph  27838  hvadd4  28021  hiassdi  28076  ocsh  28270  chj4  28522  spansncol  28555  pjjsi  28687  hoscl  28732  hodcl  28734  hoadd4  28771  homco1  28788  homulass  28789  hoadddi  28790  hoadddir  28791  unoplin  28907  adjvalval  28924  hmoplin  28929  bralnfn  28935  brafnmul  28938  lnopmi  28987  lnopcoi  28990  hmops  29007  hmopm  29008  nmophmi  29018  lnfncnbd  29044  cnlnadjlem2  29055  adjlnop  29073  adjmul  29079  adjadd  29080  branmfn  29092  kbass5  29107  kbass6  29108  leop2  29111  leopadd  29119  leopmuli  29120  pjimai  29163  atcvatlem  29372  chirredlem2  29378  mdsymlem3  29392  mdsymlem5  29394  sumdmdii  29402  sumdmdlem  29405  cdj3lem2a  29423  cdj3lem2b  29424  cdj3lem3a  29426  cdj3i  29428  xreceu  29758  toslublem  29795  tosglblem  29797  ogrpaddltbi  29847  archiabllem1b  29874  archiabllem2c  29877  archiabl  29880  slmdvsdir  29897  slmdvsass  29898  pstmxmet  30068  ordtconnlem1  30098  hasheuni  30275  omsf  30486  ballotlemirc  30721  signswmnd  30762  bnj1204  31206  txpconn  31340  cvmscld  31381  elmpps  31596  dfrdg2  31825  wsuclem  31895  nosepdm  31959  segconeu  32243  linecom  32382  linethru  32385  lineintmo  32389  fnemeet2  32487  fnejoin2  32489  lindsdom  33533  lindsenlbs  33534  matunitlindflem1  33535  matunitlindflem2  33536  heicant  33574  mblfinlem1  33576  mblfinlem3  33578  ismblfin  33580  cnambfre  33588  itg2addnclem2  33592  ftc1anclem1  33615  ftc1anclem5  33619  ftc1anclem6  33620  ftc2nc  33624  areacirclem2  33631  areacirclem4  33633  areacirclem5  33634  areacirc  33635  fzmul  33667  subspopn  33678  isbndx  33711  isbnd2  33712  isbnd3  33713  ssbnd  33717  prdstotbnd  33723  heibor1  33739  rrnmet  33758  rngonegmn1l  33870  rngohomco  33903  rngoisocnv  33910  rngoisoco  33911  crngohomfo  33935  isidlc  33944  rngoidl  33953  prnc  33996  ispridlc  33999  cvrval2  34879  glbconxN  34982  hlrelat5N  35005  cvratlem  35025  cvrat2  35033  athgt  35060  3dim2  35072  llnn0  35120  lplnn0N  35151  lvoln0N  35195  snatpsubN  35354  paddasslem18  35441  pmod1i  35452  lhpexle2  35614  lhpexle3lem  35615  lhpexle3  35616  ldilcnv  35719  trlcnv  35770  trlnidatb  35782  cdleme32snaw  36040  cdleme32fvaw  36044  cdleme42ke  36090  cdlemeg46gf  36138  cdleme50trn12  36157  cdlemg1cex  36193  cdlemb3  36211  tgrpgrplem  36354  tgrpabl  36356  tendoplcl2  36383  tendo0pl  36396  tendoicl  36401  tendoipl  36402  cdlemkid3N  36538  tendoex  36580  erngdvlem4  36596  erngdvlem4-rN  36604  dib1dim  36771  dib1dim2  36774  dihglbcpreN  36906  dihmeetALTN  36933  dih1dimatlem  36935  dihatlat  36940  oddcomabszz  37826  acongtr  37862  rpnnen3lem  37915  islssfg  37957  lmhmfgsplit  37973  unxpwdom3  37982  hbtlem7  38012  sdrgacs  38088  iocmbl  38115  ss2iundf  38268  nzss  38833  dvconstbi  38850  bccbc  38861  uzmptshftfval  38862  iccdifprioo  40060  climisp  40296  limsupresxr  40316  liminfresxr  40317  dvnmul  40476  volico  40518  volioore  40525  fourierdlem74  40715  fourierdlem75  40716  sge0iunmptlemfi  40948  sge0iunmptlemre  40950  sge0iunmpt  40953  sge0xp  40964  hspmbllem2  41162  smflimlem3  41302  smfsupmpt  41342  smfinflem  41344  smfinfmpt  41346  smflimsupmpt  41356  smfliminfmpt  41359  pfxccat1  41735  nnsum4primesodd  42009  nnsum4primesoddALTV  42010  sprsymrelfo  42072  rnghmsubcsetclem2  42301  rhmsubcsetclem2  42347  rhmsubcrngclem2  42353  lcoss  42550  snlindsntorlem  42584  aacllem  42875
  Copyright terms: Public domain W3C validator