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

Theorem 3impia 1259
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 450 . 2 (𝜑 → (𝜓 → (𝜒𝜃)))
323imp 1254 1 ((𝜑𝜓𝜒) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  w3a 1036
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 386  df-3an 1038
This theorem is referenced by:  mopick2  2538  3gencl  3232  vtoclgft  3249  mob2  3380  moi  3383  reupick3  3904  disjne  4013  elpr2elpr  4389  disji2  4627  disji  4628  tz7.2  5088  sofld  5569  ordintdif  5762  funopg  5910  fvun1  6256  fvopab6  6296  fveqressseq  6341  fvcofneq  6353  fprg  6407  2f1fvneq  6502  isores3  6570  ovmpt4g  6768  ovmpt2s  6769  ov2gf  6770  ofrval  6892  sorpssuni  6931  sorpssint  6932  poxp  7274  suppss2  7314  smoel  7442  smoord  7447  smogt  7449  oaass  7626  oewordi  7656  oeoalem  7661  oeoelem  7663  nnawordi  7686  nnaass  7687  qsel  7811  xpdom3  8043  onsdominel  8094  mapdom3  8117  fisseneq  8156  cantnflem1  8571  cfslbn  9074  cfsmolem  9077  cfcoflem  9079  infpssrlem4  9113  fin23lem7  9123  fin23lem25  9131  isf34lem7  9186  hsmexlem2  9234  axcc3  9245  axdc4lem  9262  tskss  9565  gruss  9603  gruurn  9605  gruiun  9606  gruel  9610  gruen  9619  grudomon  9624  grothac  9637  axpre-sup  9975  axsup  10098  addn0nid  10436  letrp1  10850  p1le  10851  lemul1a  10862  infrelb  10993  zextle  11435  zextlt  11436  btwnnz  11438  gtndiv  11439  uzind2  11455  fzind  11460  eluzsub  11702  zsupss  11762  xrltne  11979  lemaxle  12011  qbtwnre  12015  qbtwnxr  12016  xlemul1a  12103  icogelb  12210  iccleub  12214  iccsplit  12290  uzsubsubfz  12348  elfz0fzfz0  12428  difelfznle  12437  fvffz0  12441  elfzo0le  12495  fzonmapblen  12497  fzofzim  12498  fzosplitprm1  12561  ceile  12631  modadd1  12690  muladdmodid  12693  modmul1  12706  modirr  12724  fsuppmapnn0fiub0  12776  expcl2lem  12855  expclzlem  12867  expnegz  12877  leexp2r  12901  bcval4  13077  bccmpl  13079  hashbnd  13106  elovmpt2wrd  13330  ccatval2  13345  ccatrcl1  13359  wrdl1s1  13377  ccat2s1fvw  13397  swrdsb0eq  13429  swrdccatin1  13464  repswswrd  13512  cshwcsh2id  13555  absexpz  14026  climbdd  14383  iseraltlem2  14394  binomfallfac  14753  dvdsle  15013  divalgb  15108  ndvdssub  15114  dvdsgcd  15242  rplpwr  15257  lcmgcdlem  15300  lcmfunsn  15338  coprmdvds1  15346  qredeq  15352  prmdvdsexpr  15410  nnnn0modprm0  15492  prm23ge5  15501  pcexp  15545  difsqpwdvds  15572  prmpwdvds  15589  ramcl  15714  cshwshashlem3  15785  cshwrepswhash1  15790  elrestr  16070  xpscfv  16203  mreintcl  16236  mremre  16245  mrieqv2d  16280  initoeu2lem1  16645  funcestrcsetclem9  16769  funcsetcestrclem9  16784  prstr  16914  drsdirfi  16919  latnlej  17049  latnlej2  17052  acsdrsel  17148  acsdrscl  17151  mrelatglb  17165  mrelatlub  17167  isnmgm  17227  grpasscan1  17459  grpinvnz  17467  mulgneg2  17556  gsmsymgrfix  17829  f1omvdco2  17849  symggen  17871  odcl2  17963  odhash3  17972  lsmss1  18060  lsmss2  18062  efgred  18142  efgcpbl  18150  ablfacrp  18446  ablfac1eu  18453  ablfaclem3  18467  dvdsrmul1  18634  dvdsunit  18644  irredmul  18690  lmodlema  18849  ply1scln0  19642  psgnodpmr  19917  lindsss  20144  lindfmm  20147  dmatelnd  20283  mdetdiaglem  20385  mdet0  20393  mdetunilem7  20405  slesolinv  20467  cramerimplem3  20472  cpmatpmat  20496  m2cpminvid2lem  20540  chfacfscmul0  20644  chfacfpmmul0  20648  riinopn  20694  clsndisj  20860  cnpf2  21035  hausnei2  21138  cmpcov  21173  cmpfii  21193  unconn  21213  t1connperf  21220  nrmr0reg  21533  fbfinnfr  21626  filuni  21670  alexsubALT  21836  tmdgsum  21880  cuspcvg  22086  mopni  22278  isngp4  22397  metdsre  22637  iimulcl  22717  phtpc01  22777  clmmulg  22882  cfilucfil4  23099  bcthlem5  23106  bcth  23107  bcth3  23109  itg1le  23461  itg2le  23487  bddmulibl  23586  dvnres  23675  cpnord  23679  dvnfre  23696  deg1ge  23839  dgr1term  23997  aaliou3lem2  24079  sincosq1lem  24230  cxpge0  24410  cxpmul2  24416  logrec  24482  sqfpc  24844  bcmono  24983  gausslemma2dlem1a  25071  gausslemma2dlem2  25073  gausslemma2dlem4  25075  2lgsoddprmlem3  25120  pntrmax  25234  qabvexp  25296  ostth2lem2  25304  ax5seglem4  25793  axeuclidlem  25823  uhgredgrnv  26006  usgredg4  26090  nbuhgr2vtx1edgblem  26228  vtxduhgr0e  26355  vtxduhgr0nedg  26369  rusgrpropnb  26460  uspgr2wlkeqi  26525  redwlklem  26549  lfgrwlkprop  26565  2pthnloop  26608  spthonepeq  26629  pthdlem2lem  26644  crctcshwlkn0lem3  26685  crctcshwlkn0lem5  26687  crctcshwlkn0lem7  26689  crctcshwlkn0  26694  wlkiswwlks1  26734  wlkiswwlks2  26742  wlkiswwlksupgr2  26744  wwlksnext  26769  wwlksnextproplem2  26786  wspthsnonn0vne  26794  2pthon3v  26820  rusgrnumwwlk  26851  wwlksext2clwwlk  26904  erclwwlkseqlen  26913  erclwwlkssym  26915  erclwwlkstr  26916  erclwwlksneqlen  26925  erclwwlksnsym  26927  erclwwlksntr  26928  uhgr3cyclex  27022  upgreupthseg  27049  eupth2lem3lem4  27071  eucrctshift  27083  4cycl2vnunb  27134  nvs  27488  nvtri  27495  nmlno0  27620  nmlnoubi  27621  ubth  27699  hlipgt0  27740  ocnel  28127  elspansn2  28396  elspansn3  28401  normcan  28405  pjoml2  28440  lecm  28446  osum  28474  nmbdfnlb  28879  leopmul  28963  hstpyth  29058  cvnbtwn  29115  ssmd1  29140  ssmd2  29141  ssdmd1  29142  ssdmd2  29143  cvmd  29165  cvdmd  29166  superpos  29183  disji2f  29362  disjif  29363  disjif2  29366  padct  29471  ffs2  29477  bcm1n  29528  omndadd  29680  ogrpaddlt  29692  archiabl  29726  slmdlema  29730  eulerpartlemb  30404  sgn3da  30577  cvmsdisj  31226  cvmlift2lem12  31270  br1steqg  31648  br2ndeqg  31649  poseq  31724  nosepon  31792  nolesgn2o  31798  nosepnelem  31804  nosepne  31805  nosepdmlem  31807  nosepdm  31808  nodenselem8  31815  noresle  31820  noetalem3  31839  sslttr  31888  scutbdaylt  31896  lineintmo  32239  nn0prpwlem  32292  nn0prpw  32293  neibastop2lem  32330  bddiblnc  33451  areacirc  33476  incsequz  33515  mettrifi  33524  ismtybnd  33577  heiborlem1  33581  rngoisocnv  33751  risci  33757  lfl1  34176  lkrlsp2  34209  omlfh3N  34365  cvrnbtwn  34377  cvrnbtwn2  34381  cvrnbtwn4  34385  cvlexch3  34438  cvlexch4N  34439  cvlatexchb1  34440  2llnne2N  34513  atcvrj0  34533  cvrat2  34534  ps-1  34582  3atlem5  34592  islln2a  34622  lplnriaN  34655  lplnribN  34656  llncvrlpln2  34662  lplncvrlvol2  34720  psubatN  34860  pmapglb2N  34876  pmapglb2xN  34877  2llnma1b  34891  paddasslem17  34941  pmod2iN  34954  pmodl42N  34956  hlmod1i  34961  atmod1i1  34962  atmod1i2  34964  llnmod1i2  34965  pclcmpatN  35006  osumcllem8N  35068  pexmidlem3N  35077  pl42lem4N  35087  4atexlem7  35180  ltrnnid  35241  cdlemc4  35300  cdleme32a  35548  cdlemeg46gfre  35639  cdlemf2  35669  cdlemg4c  35719  trlcoat  35830  tendovalco  35872  tendoeq2  35881  cdlemk36  36020  diael  36151  diatrl  36152  dicelval1stN  36296  dicelval2nd  36297  dihlspsnat  36441  dochkr1  36586  lcfrlem9  36658  mapdh8e  36892  hdmapval0  36944  hgmapval0  37003  incssnn0  37093  pell14qrexpcl  37250  pell14qrgap  37258  congadd  37352  acongsym  37362  acongtr  37364  dvdsacongtr  37370  jm2.19lem3  37377  jm2.19lem4  37378  jm2.26lem3  37387  relexpiidm  37815  bi13impia  38514  3impcombi  38864  ioogtlb  39520  iocgtlb  39527  iocleub  39528  icoltub  39535  iooltub  39538  limclner  39683  limsupre3lem  39764  climuzlem  39775  elfzelfzlble  41094  subsubelfzo0  41099  iccpartigtl  41123  pfx2  41177  pfxccatpfx2  41193  sqrtpwpw2p  41215  fmtnoprmfac1lem  41241  fmtno4prmfac  41249  evenltle  41391  even3prm2  41393  wtgoldbnnsum4prm  41455  bgoldbnnsum3prm  41457  bgoldbtbndlem1  41458  bgoldbtbndlem3  41460  bgoldbtbndlem4  41461  bgoldbtbnd  41462  upgrwlkupwlk  41486  c0snmgmhm  41679  funcringcsetcALTV2lem9  41809  funcringcsetclem9ALTV  41832  lincscmcl  41986  lindslinindimp2lem4  42015  lincresunit2  42032  lincresunit3  42035  elfzolborelfzop1  42074  m1modmmod  42081  rege1logbzge0  42118  fllog2  42127  dignn0ldlem  42161
  Copyright terms: Public domain W3C validator