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

Theorem 3impia 1280
Description: Importation to triple conjunction. (Contributed by NM, 13-Jun-2006.)
Hypothesis
Ref Expression
3impia.1 ((𝜑𝜓) → (𝜒𝜃))
Assertion
Ref Expression
3impia ((𝜑𝜓𝜒) → 𝜃)

Proof of Theorem 3impia
StepHypRef Expression
1 3impia.1 . . 3 ((𝜑𝜓) → (𝜒𝜃))
21ex 449 . 2 (𝜑 → (𝜓 → (𝜒𝜃)))
323imp 1275 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:  mopick2  2569  3gencl  3268  vtoclgft  3285  mob2  3419  moi  3422  reupick3  3945  disjne  4055  elpr2elpr  4429  disji2  4668  disji  4669  tz7.2  5127  sofld  5616  ordintdif  5812  funopg  5960  fvun1  6308  fvopab6  6350  fveqressseq  6395  fvcofneq  6407  fprg  6462  2f1fvneq  6557  isores3  6625  ovmpt4g  6825  ovmpt2s  6826  ov2gf  6827  ofrval  6949  sorpssuni  6988  sorpssint  6989  poxp  7334  suppss2  7374  smoel  7502  smoord  7507  smogt  7509  oaass  7686  oewordi  7716  oeoalem  7721  oeoelem  7723  nnawordi  7746  nnaass  7747  qsel  7869  xpdom3  8099  onsdominel  8150  mapdom3  8173  fisseneq  8212  cantnflem1  8624  cfslbn  9127  cfsmolem  9130  cfcoflem  9132  infpssrlem4  9166  fin23lem7  9176  fin23lem25  9184  isf34lem7  9239  hsmexlem2  9287  axcc3  9298  axdc4lem  9315  tskss  9618  gruss  9656  gruurn  9658  gruiun  9659  gruel  9663  gruen  9672  grudomon  9677  grothac  9690  axpre-sup  10028  axsup  10151  addn0nid  10489  letrp1  10903  p1le  10904  lemul1a  10915  infrelb  11046  zextle  11488  zextlt  11489  btwnnz  11491  gtndiv  11492  uzind2  11508  fzind  11513  eluzsub  11755  zsupss  11815  xrltne  12032  lemaxle  12064  qbtwnre  12068  qbtwnxr  12069  xlemul1a  12156  icogelb  12263  iccleub  12267  iccsplit  12343  uzsubsubfz  12401  elfz0fzfz0  12483  difelfznle  12492  fvffz0  12496  elfzo0le  12551  fzonmapblen  12553  fzofzim  12554  ceile  12688  modadd1  12747  muladdmodid  12750  modmul1  12763  modirr  12781  fsuppmapnn0fiub0  12833  expcl2lem  12912  expclzlem  12924  expnegz  12934  leexp2r  12958  bcval4  13134  bccmpl  13136  hashbnd  13163  elovmpt2wrd  13380  ccatval2  13396  ccatrcl1  13412  wrdl1s1  13431  ccat2s1fvw  13460  swrdsb0eq  13493  swrdccatin1  13529  repswswrd  13577  cshwcsh2id  13620  absexpz  14089  climbdd  14446  iseraltlem2  14457  binomfallfac  14816  dvdsle  15079  divalgb  15174  ndvdssub  15180  dvdsgcd  15308  rplpwr  15323  lcmgcdlem  15366  lcmfunsn  15404  coprmdvds1  15412  qredeq  15418  prmdvdsexpr  15476  nnnn0modprm0  15558  prm23ge5  15567  pcexp  15611  difsqpwdvds  15638  prmpwdvds  15655  ramcl  15780  cshwshashlem3  15851  cshwrepswhash1  15856  elrestr  16136  xpscfv  16269  mreintcl  16302  mremre  16311  mrieqv2d  16346  initoeu2lem1  16711  funcestrcsetclem9  16835  funcsetcestrclem9  16850  prstr  16980  drsdirfi  16985  latnlej  17115  latnlej2  17118  acsdrsel  17214  acsdrscl  17217  mrelatglb  17231  mrelatlub  17233  isnmgm  17293  grpasscan1  17525  grpinvnz  17533  mulgneg2  17622  gsmsymgrfix  17894  f1omvdco2  17914  symggen  17936  odcl2  18028  odhash3  18037  lsmss1  18125  lsmss2  18127  efgred  18207  efgcpbl  18215  ablfacrp  18511  ablfac1eu  18518  ablfaclem3  18532  dvdsrmul1  18699  dvdsunit  18709  irredmul  18755  lmodlema  18916  ply1scln0  19709  psgnodpmr  19984  lindsss  20211  lindfmm  20214  dmatelnd  20350  mdetdiaglem  20452  mdet0  20460  mdetunilem7  20472  slesolinv  20534  cramerimplem3  20539  cpmatpmat  20563  m2cpminvid2lem  20607  chfacfscmul0  20711  chfacfpmmul0  20715  riinopn  20761  clsndisj  20927  cnpf2  21102  hausnei2  21205  cmpcov  21240  cmpfii  21260  unconn  21280  t1connperf  21287  nrmr0reg  21600  fbfinnfr  21692  filuni  21736  alexsubALT  21902  tmdgsum  21946  cuspcvg  22152  mopni  22344  isngp4  22463  metdsre  22703  iimulcl  22783  phtpc01  22842  clmmulg  22947  cfilucfil4  23164  bcthlem5  23171  bcth  23172  bcth3  23174  itg1le  23525  itg2le  23551  bddmulibl  23650  dvnres  23739  cpnord  23743  dvnfre  23760  deg1ge  23903  dgr1term  24061  aaliou3lem2  24143  sincosq1lem  24294  cxpge0  24474  cxpmul2  24480  logrec  24546  sqfpc  24908  bcmono  25047  gausslemma2dlem1a  25135  gausslemma2dlem2  25137  gausslemma2dlem4  25139  2lgsoddprmlem3  25184  pntrmax  25298  qabvexp  25360  ostth2lem2  25368  ax5seglem4  25857  axeuclidlem  25887  uhgredgrnv  26070  usgredg4  26154  nbuhgr2vtx1edgblem  26292  vtxduhgr0e  26430  vtxduhgr0nedg  26444  rusgrpropnb  26535  uspgr2wlkeqi  26600  redwlklem  26624  lfgrwlkprop  26640  2pthnloop  26683  spthonepeq  26704  pthdlem2lem  26719  crctcshwlkn0lem3  26760  crctcshwlkn0lem5  26762  crctcshwlkn0lem7  26764  crctcshwlkn0  26769  wlkiswwlks1  26821  wlkiswwlks2  26829  wlkiswwlksupgr2  26831  wwlksnext  26856  wwlksnextproplem2  26873  wspthsnonn0vne  26882  2pthon3v  26908  rusgrnumwwlk  26942  erclwwlkeqlen  26976  erclwwlksym  26978  erclwwlktr  26979  wwlksext2clwwlkOLD  27022  erclwwlkneqlen  27032  erclwwlknsym  27034  erclwwlkntr  27035  uhgr3cyclex  27160  upgreupthseg  27187  eupth2lem3lem4  27209  eucrctshift  27221  4cycl2vnunb  27270  nvs  27646  nvtri  27653  nmlno0  27778  nmlnoubi  27779  ubth  27857  hlipgt0  27898  ocnel  28285  elspansn2  28554  elspansn3  28559  normcan  28563  pjoml2  28598  lecm  28604  osum  28632  nmbdfnlb  29037  leopmul  29121  hstpyth  29216  cvnbtwn  29273  ssmd1  29298  ssmd2  29299  ssdmd1  29300  ssdmd2  29301  cvmd  29323  cvdmd  29324  superpos  29341  disji2f  29516  disjif  29517  disjif2  29520  padct  29625  ffs2  29631  bcm1n  29682  omndadd  29834  ogrpaddlt  29846  archiabl  29880  slmdlema  29884  eulerpartlemb  30558  sgn3da  30731  cvmsdisj  31378  cvmlift2lem12  31422  br1steqgOLD  31798  br2ndeqgOLD  31799  poseq  31878  nosepon  31943  nolesgn2o  31949  nosepnelem  31955  nosepne  31956  nosepdmlem  31958  nosepdm  31959  nodenselem8  31966  noresle  31971  noetalem3  31990  sslttr  32039  scutbdaylt  32047  lineintmo  32389  nn0prpwlem  32442  nn0prpw  32443  neibastop2lem  32480  bddiblnc  33610  areacirc  33635  incsequz  33674  mettrifi  33683  ismtybnd  33736  heiborlem1  33740  rngoisocnv  33910  risci  33916  lfl1  34675  lkrlsp2  34708  omlfh3N  34864  cvrnbtwn  34876  cvrnbtwn2  34880  cvrnbtwn4  34884  cvlexch3  34937  cvlexch4N  34938  cvlatexchb1  34939  2llnne2N  35012  atcvrj0  35032  cvrat2  35033  ps-1  35081  3atlem5  35091  islln2a  35121  lplnriaN  35154  lplnribN  35155  llncvrlpln2  35161  lplncvrlvol2  35219  psubatN  35359  pmapglb2N  35375  pmapglb2xN  35376  2llnma1b  35390  paddasslem17  35440  pmod2iN  35453  pmodl42N  35455  hlmod1i  35460  atmod1i1  35461  atmod1i2  35463  llnmod1i2  35464  pclcmpatN  35505  osumcllem8N  35567  pexmidlem3N  35576  pl42lem4N  35586  4atexlem7  35679  ltrnnid  35740  cdlemc4  35799  cdleme32a  36046  cdlemeg46gfre  36137  cdlemf2  36167  cdlemg4c  36217  trlcoat  36328  tendovalco  36370  tendoeq2  36379  cdlemk36  36518  diael  36649  diatrl  36650  dicelval1stN  36794  dicelval2nd  36795  dihlspsnat  36939  dochkr1  37084  lcfrlem9  37156  mapdh8e  37390  hdmapval0  37442  hgmapval0  37501  incssnn0  37591  pell14qrexpcl  37748  pell14qrgap  37756  congadd  37850  acongsym  37860  acongtr  37862  dvdsacongtr  37868  jm2.19lem3  37875  jm2.19lem4  37876  jm2.26lem3  37885  relexpiidm  38313  bi13impia  39011  3impcombi  39361  ioogtlb  40035  iocgtlb  40042  iocleub  40043  icoltub  40050  iooltub  40053  limclner  40201  limsupre3lem  40282  climuzlem  40293  elfzelfzlble  41656  subsubelfzo0  41661  iccpartigtl  41684  pfx2  41737  pfxccatpfx2  41753  sqrtpwpw2p  41775  fmtnoprmfac1lem  41801  fmtno4prmfac  41809  evenltle  41951  even3prm2  41953  wtgoldbnnsum4prm  42015  bgoldbnnsum3prm  42017  bgoldbtbndlem1  42018  bgoldbtbndlem3  42020  bgoldbtbndlem4  42021  bgoldbtbnd  42022  upgrwlkupwlk  42046  c0snmgmhm  42239  funcringcsetcALTV2lem9  42369  funcringcsetclem9ALTV  42392  lincscmcl  42546  lindslinindimp2lem4  42575  lincresunit2  42592  lincresunit3  42595  elfzolborelfzop1  42634  m1modmmod  42641  rege1logbzge0  42678  fllog2  42687  dignn0ldlem  42721
  Copyright terms: Public domain W3C validator