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

Theorem 3impia 1252
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 448 . 2 (𝜑 → (𝜓 → (𝜒𝜃)))
323imp 1248 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:  mopick2  2523  3gencl  3205  vtoclgft  3222  mob2  3348  moi  3351  reupick3  3866  disjne  3969  disji2  4559  disji  4560  tz7.2  5008  sofld  5482  ordintdif  5673  funopg  5818  fvun1  6160  fvopab6  6199  fveqressseq  6244  fvcofneq  6256  fprg  6301  isores3  6459  ovmpt4g  6655  ovmpt2s  6656  ov2gf  6657  ofrval  6778  sorpssuni  6817  sorpssint  6818  poxp  7149  suppss2  7189  smoel  7317  smoord  7322  smogt  7324  oaass  7501  oewordi  7531  oeoalem  7536  oeoelem  7538  nnawordi  7561  nnaass  7562  qsel  7686  xpdom3  7916  onsdominel  7967  mapdom3  7990  fisseneq  8029  cantnflem1  8442  cfslbn  8945  cfsmolem  8948  cfcoflem  8950  infpssrlem4  8984  fin23lem7  8994  fin23lem25  9002  isf34lem7  9057  hsmexlem2  9105  axcc3  9116  axdc4lem  9133  tskss  9432  gruss  9470  gruurn  9472  gruiun  9473  gruel  9477  gruen  9486  grudomon  9491  grothac  9504  axpre-sup  9842  axsup  9960  addn0nid  10298  letrp1  10710  p1le  10711  lemul1a  10722  infrelb  10851  zextle  11278  zextlt  11279  btwnnz  11281  gtndiv  11282  uzind2  11298  fzind  11303  eluzsub  11545  zsupss  11605  xrltne  11825  lemaxle  11855  qbtwnre  11859  qbtwnxr  11860  xlemul1a  11943  icogelb  12048  iccleub  12052  iccsplit  12128  uzsubsubfz  12185  elfz0fzfz0  12264  difelfznle  12273  fvffz0  12277  elfzo0le  12330  fzonmapblen  12332  fzofzim  12333  fzosplitprm1  12394  ceile  12461  modadd1  12520  muladdmodid  12523  modmul1  12536  modirr  12554  fsuppmapnn0fiub0  12606  expcl2lem  12685  expclzlem  12697  expnegz  12707  leexp2r  12731  bcval4  12907  bccmpl  12909  hashbnd  12936  elovmpt2wrd  13144  ccatval2  13157  ccatrcl1  13171  wrdl1s1  13189  ccat2s1fvw  13209  swrdsb0eq  13241  swrdccatin1  13276  repswswrd  13324  cshwcsh2id  13367  absexpz  13835  climbdd  14192  iseraltlem2  14203  binomfallfac  14553  dvdsle  14812  divalgb  14907  ndvdssub  14913  dvdsgcd  15041  rplpwr  15056  lcmgcdlem  15099  lcmfunsn  15137  coprmdvds1  15145  qredeq  15151  prmdvdsexpr  15209  nnnn0modprm0  15291  prm23ge5  15300  pcexp  15344  difsqpwdvds  15371  prmpwdvds  15388  ramcl  15513  cshwshashlem3  15584  cshwrepswhash1  15589  elrestr  15854  xpscfv  15987  mreintcl  16020  mremre  16029  mrieqv2d  16064  initoeu2lem1  16429  funcestrcsetclem9  16553  funcsetcestrclem9  16568  prstr  16698  drsdirfi  16703  latnlej  16833  latnlej2  16836  acsdrsel  16932  acsdrscl  16935  mrelatglb  16949  mrelatlub  16951  isnmgm  17011  grpasscan1  17243  grpinvnz  17251  mulgneg2  17340  gsmsymgrfix  17613  f1omvdco2  17633  symggen  17655  odcl2  17747  odhash3  17756  lsmss1  17844  lsmss2  17846  efgred  17926  efgcpbl  17934  ablfacrp  18230  ablfac1eu  18237  ablfaclem3  18251  dvdsrmul1  18418  dvdsunit  18428  irredmul  18474  lmodlema  18633  ply1scln0  19424  psgnodpmr  19696  lindsss  19920  lindfmm  19923  dmatelnd  20059  mdetdiaglem  20161  mdet0  20169  mdetunilem7  20181  slesolinv  20243  cramerimplem3  20248  cpmatpmat  20272  m2cpminvid2lem  20316  chfacfscmul0  20420  chfacfpmmul0  20424  riinopn  20476  clsndisj  20627  cnpf2  20802  hausnei2  20905  cmpcov  20940  cmpfii  20960  uncon  20980  t1conperf  20987  nrmr0reg  21300  fbfinnfr  21393  filuni  21437  alexsubALT  21603  tmdgsum  21647  cuspcvg  21853  mopni  22044  isngp4  22162  metdsre  22391  iimulcl  22471  phtpc01  22531  clmmulg  22636  cfilucfil4  22839  bcthlem5  22846  bcth  22847  bcth3  22849  itg1le  23199  itg2le  23225  bddmulibl  23324  dvnres  23413  cpnord  23417  dvnfre  23434  deg1ge  23575  dgr1term  23733  aaliou3lem2  23815  sincosq1lem  23966  cxpge0  24142  cxpmul2  24148  logrec  24214  sqfpc  24576  bcmono  24715  gausslemma2dlem1a  24803  gausslemma2dlem2  24805  gausslemma2dlem4  24807  2lgsoddprmlem3  24852  pntrmax  24966  qabvexp  25028  ostth2lem2  25036  ax5seglem4  25526  axeuclidlem  25556  edgwlk  25821  usgra2wlkspthlem1  25909  usgra2wlkspthlem2  25910  wwlknimp  25977  wlkiswwlk1  25980  wlkiswwlk2  25987  wwlknext  26014  wwlkextproplem2  26032  wwlkext2clwwlk  26093  erclwwlkeqlen  26102  erclwwlksym  26104  erclwwlktr  26105  erclwwlkneqlen  26114  erclwwlknsym  26116  erclwwlkntr  26117  usg2wotspth  26173  usgfiregdegfi  26200  rusgraprop2  26231  rusgraprop3  26232  rusgranumwlk  26246  4cycl2vnunb  26306  usgn0fidegnn0  26318  nvs  26691  nvtri  26699  nmlno0  26836  nmlnoubi  26837  ubth  26915  hlipgt0  26956  ocnel  27343  elspansn2  27612  elspansn3  27617  normcan  27621  pjoml2  27656  lecm  27662  osum  27690  nmbdfnlb  28095  leopmul  28179  hstpyth  28274  cvnbtwn  28331  ssmd1  28356  ssmd2  28357  ssdmd1  28358  ssdmd2  28359  cvmd  28381  cvdmd  28382  superpos  28399  disji2f  28574  disjif  28575  disjif2  28578  padct  28687  ffs2  28693  bcm1n  28743  omndadd  28839  ogrpaddlt  28851  archiabl  28885  slmdlema  28889  eulerpartlemb  29559  sgn3da  29732  cvmsdisj  30308  cvmlift2lem12  30352  br1steqg  30721  br2ndeqg  30722  poseq  30796  nosepon  30868  nodenselem8  30889  nofulllem4  30906  lineintmo  31236  nn0prpwlem  31289  nn0prpw  31290  neibastop2lem  31327  bddiblnc  32449  areacirc  32474  incsequz  32513  mettrifi  32522  ismtybnd  32575  heiborlem1  32579  rngoisocnv  32749  risci  32755  lfl1  33174  lkrlsp2  33207  omlfh3N  33363  cvrnbtwn  33375  cvrnbtwn2  33379  cvrnbtwn4  33383  cvlexch3  33436  cvlexch4N  33437  cvlatexchb1  33438  2llnne2N  33511  atcvrj0  33531  cvrat2  33532  ps-1  33580  3atlem5  33590  islln2a  33620  lplnriaN  33653  lplnribN  33654  llncvrlpln2  33660  lplncvrlvol2  33718  psubatN  33858  pmapglb2N  33874  pmapglb2xN  33875  2llnma1b  33889  paddasslem17  33939  pmod2iN  33952  pmodl42N  33954  hlmod1i  33959  atmod1i1  33960  atmod1i2  33962  llnmod1i2  33963  pclcmpatN  34004  osumcllem8N  34066  pexmidlem3N  34075  pl42lem4N  34085  4atexlem7  34178  ltrnnid  34239  cdlemc4  34298  cdleme32a  34546  cdlemeg46gfre  34637  cdlemf2  34667  cdlemg4c  34717  trlcoat  34828  tendovalco  34870  tendoeq2  34879  cdlemk36  35018  diael  35149  diatrl  35150  dicelval1stN  35294  dicelval2nd  35295  dihlspsnat  35439  dochkr1  35584  lcfrlem9  35656  mapdh8e  35890  hdmapval0  35942  hgmapval0  36001  incssnn0  36091  pell14qrexpcl  36248  pell14qrgap  36256  congadd  36350  acongsym  36360  acongtr  36362  dvdsacongtr  36368  jm2.19lem3  36375  jm2.19lem4  36376  jm2.26lem3  36385  relexpiidm  36814  bi13impia  37514  3impcombi  37864  ioogtlb  38364  iocgtlb  38371  iocleub  38372  icoltub  38379  iooltub  38382  limclner  38518  iccpartigtl  39762  sqrtpwpw2p  39789  fmtnoprmfac1lem  39815  fmtno4prmfac  39823  wtgoldbnnsum4prm  40019  bgoldbnnsum3prm  40021  bgoldbtbndlem1  40022  bgoldbtbndlem3  40024  bgoldbtbndlem4  40025  bgoldbtbnd  40026  pfx2  40076  pfxccatpfx2  40092  elpr2elpr  40126  2f1fvneq  40134  elfzelfzlble  40181  subsubelfzo0  40182  uhgredgrnv  40361  usgredg4  40442  nbuhgr2vtx1edgblem  40571  vtxduhgr0e  40691  vtxduhgr0nedg  40705  rusgrpropnb  40781  upgr1wlkwlk  40845  uspgr2wlkeqi  40854  red1wlklem  40878  lfgrwlkprop  40894  2pthnloop  40935  spthonepeq-av  40956  pthdlem2lem  40971  crctcsh1wlkn0lem3  41013  crctcsh1wlkn0lem5  41015  crctcsh1wlkn0lem7  41017  crctcsh1wlkn0  41022  1wlkiswwlks1  41062  1wlkiswwlks2  41070  1wlkiswwlksupgr2  41072  wwlksnext  41097  wwlksnextproplem2  41114  wspthsnonn0vne  41122  2pthon3v-av  41148  rusgrnumwwlk  41176  wwlksext2clwwlk  41229  erclwwlkseqlen  41238  erclwwlkssym  41240  erclwwlkstr  41241  erclwwlksneqlen  41250  erclwwlksnsym  41252  erclwwlksntr  41253  uhgr3cyclex  41347  upgreupthseg  41375  eupth2lem3lem4  41397  eucrctshift  41409  4cycl2vnunb-av  41458  c0snmgmhm  41702  funcringcsetcALTV2lem9  41834  funcringcsetclem9ALTV  41857  lincscmcl  42013  lindslinindimp2lem4  42042  lincresunit2  42059  lincresunit3  42062  elfzolborelfzop1  42101  m1modmmod  42108  rege1logbzge0  42149  fllog2  42158  dignn0ldlem  42192
  Copyright terms: Public domain W3C validator