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

Theorem 3impia 1114
Description: Importation to triple conjunction. (Contributed by NM, 13-Jun-2006.) (Proof shortened by Wolf Lammen, 21-Jun-2022.)
Hypothesis
Ref Expression
3impia.1 ((𝜑𝜓) → (𝜒𝜃))
Assertion
Ref Expression
3impia ((𝜑𝜓𝜒) → 𝜃)

Proof of Theorem 3impia
StepHypRef Expression
1 3impia.1 . . 3 ((𝜑𝜓) → (𝜒𝜃))
21expimpd 457 . 2 (𝜑 → ((𝜓𝜒) → 𝜃))
323impib 1113 1 ((𝜑𝜓𝜒) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399  w3a 1084
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 210  df-an 400  df-3an 1086
This theorem is referenced by:  mopick2  2702  3gencl  3486  vtoclgft  3504  vtoclgftOLD  3505  mob2  3657  moi  3660  reupick3  4243  disjne  4365  elpr2elpr  4762  disji2  5015  disji  5016  tz7.2  5507  sofld  6015  ordintdif  6212  funopg  6362  fvun1  6733  fvopab6  6782  fveqressseq  6828  fvcofneq  6840  fprg  6898  2f1fvneq  7000  isores3  7071  ovmpt4g  7280  ovmpos  7281  ov2gf  7282  ofrval  7403  sorpssuni  7442  sorpssint  7443  poxp  7809  suppss2  7851  smoel  7984  smoord  7989  smogt  7991  oaass  8174  oewordi  8204  oeoalem  8209  oeoelem  8211  nnawordi  8234  nnaass  8235  qsel  8363  xpdom3  8602  onsdominel  8654  mapdom3  8677  fisseneq  8717  cantnflem1  9140  cfslbn  9682  cfsmolem  9685  cfcoflem  9687  infpssrlem4  9721  fin23lem7  9731  fin23lem25  9739  isf34lem7  9794  hsmexlem2  9842  axcc3  9853  axdc4lem  9870  tskss  10173  gruss  10211  gruurn  10213  gruiun  10214  gruel  10218  gruen  10227  grudomon  10232  grothac  10245  axpre-sup  10584  axsup  10709  addn0nid  11053  letrp1  11477  p1le  11478  lemul1a  11487  infrelb  11617  zextle  12047  zextlt  12048  btwnnz  12050  gtndiv  12051  uzind2  12067  fzind  12072  eluzsub  12266  zsupss  12329  xrltne  12548  lemaxle  12580  qbtwnre  12584  qbtwnxr  12585  xlemul1a  12673  icogelb  12780  iccleub  12784  iccsplit  12867  uzsubsubfz  12928  elfz0fzfz0  13011  difelfznle  13020  fvffz0  13024  elfzo0le  13080  fzonmapblen  13082  fzofzim  13083  ceile  13216  modadd1  13275  muladdmodid  13278  modmul1  13291  modirr  13309  fsuppmapnn0fiub0  13360  expcl2lem  13441  expclzlem  13453  expnegz  13463  leexp2r  13538  bcval4  13667  bccmpl  13669  hashbnd  13696  hashunsnggt  13755  hashgt23el  13785  elovmpowrd  13905  ccatval2  13927  ccatrcl1  13943  wrdl1s1  13963  ccat2s1fvw  13993  ccat2s1fvwOLD  13994  swrdsb0eq  14020  swrdccatin1  14082  pfxccatpfx2  14094  repswswrd  14141  cshwcsh2id  14185  absexpz  14661  climbdd  15024  iseraltlem2  15035  binomfallfac  15391  dvdsle  15656  divalgb  15749  ndvdssub  15754  dvdsgcd  15886  dfgcd2  15888  rplpwr  15901  lcmgcdlem  15944  lcmfunsn  15982  coprmdvds1  15990  qredeq  15995  2mulprm  16031  prmdvdsexpr  16055  nnnn0modprm0  16137  prm23ge5  16146  pcexp  16190  difsqpwdvds  16217  prmpwdvds  16234  ramcl  16359  cshwshashlem3  16427  cshwrepswhash1  16432  elrestr  16698  mreintcl  16862  mremre  16871  mrieqv2d  16906  initoeu2lem1  17270  funcestrcsetclem9  17394  funcsetcestrclem9  17409  prstr  17539  drsdirfi  17544  latnlej  17674  latnlej2  17677  acsdrsel  17773  acsdrscl  17776  mrelatglb  17790  mrelatlub  17792  isnmgm  17852  grpasscan1  18158  grpinvnz  18166  mulgneg2  18257  gsmsymgrfix  18552  f1omvdco2  18572  symggen  18594  odcl2  18688  odhash3  18697  lsmss1  18787  lsmss2  18789  efgred  18870  efgcpbl  18878  ablfacrp  19185  ablfac1eu  19192  ablfaclem3  19206  dvdsrmul1  19403  dvdsunit  19413  irredmul  19459  lmodlema  19636  psgnodpmr  20283  phlssphl  20352  lindsss  20517  lindfmm  20520  ply1scln0  20924  dmatelnd  21105  mdetdiaglem  21207  mdet0  21215  mdetunilem7  21227  slesolinv  21289  cramerimplem3  21294  cpmatpmat  21319  m2cpminvid2lem  21363  chfacfscmul0  21467  chfacfpmmul0  21471  riinopn  21517  clsndisj  21684  cnpf2  21859  hausnei2  21962  cmpcov  21998  cmpfii  22018  unconn  22038  t1connperf  22045  nrmr0reg  22358  fbfinnfr  22450  filuni  22494  alexsubALT  22660  tmdgsum  22704  cuspcvg  22911  mopni  23103  isngp4  23222  metdsre  23462  iimulcl  23546  phtpc01  23605  clmmulg  23710  cfilucfil4  23929  bcthlem5  23936  bcth  23937  bcth3  23939  itg1le  24321  itg2le  24347  bddmulibl  24446  bddiblnc  24449  dvnres  24538  cpnord  24542  dvnfre  24559  deg1ge  24703  dgr1term  24861  aaliou3lem2  24943  sincosq1lem  25094  cxpge0  25278  cxpmul2  25284  logrec  25353  logbgcd1irr  25384  sqfpc  25726  bcmono  25865  gausslemma2dlem1a  25953  gausslemma2dlem2  25955  gausslemma2dlem4  25957  2lgsoddprmlem3  26002  pntrmax  26152  qabvexp  26214  ostth2lem2  26222  ax5seglem4  26730  axeuclidlem  26760  uhgredgrnv  26927  usgredg4  27011  nbuhgr2vtx1edgblem  27145  vtxduhgr0e  27272  vtxduhgr0nedg  27286  rusgrpropnb  27377  uspgr2wlkeqi  27441  redwlklem  27465  lfgrwlkprop  27481  2pthnloop  27524  spthonepeq  27545  pthdlem2lem  27560  crctcshwlkn0lem3  27602  crctcshwlkn0lem5  27604  crctcshwlkn0lem7  27606  crctcshwlkn0  27611  wlkiswwlks1  27657  wlkiswwlks2  27665  wlkiswwlksupgr2  27667  wwlksnext  27683  wwlksnextproplem2  27700  wspthsnonn0vne  27707  2pthon3v  27733  rusgrnumwwlk  27765  erclwwlkeqlen  27808  erclwwlksym  27810  erclwwlktr  27811  erclwwlkneqlen  27857  erclwwlknsym  27859  erclwwlkntr  27860  uhgr3cyclex  27971  upgreupthseg  27998  eupth2lem3lem4  28020  eucrctshift  28032  4cycl2vnunb  28079  nvs  28450  nvtri  28457  nmlno0  28582  nmlnoubi  28583  ubth  28660  hlipgt0  28701  ocnel  29085  elspansn2  29354  elspansn3  29359  normcan  29363  pjoml2  29398  lecm  29404  osum  29432  nmbdfnlb  29837  leopmul  29921  hstpyth  30016  cvnbtwn  30073  ssmd1  30098  ssmd2  30099  ssdmd1  30100  ssdmd2  30101  cvmd  30123  cvdmd  30124  superpos  30141  disji2f  30344  disjif  30345  disjif2  30348  preiman0  30473  padct  30485  ffs2  30494  bcm1n  30548  s2f1  30651  omndadd  30761  ogrpaddlt  30772  archiabl  30881  slmdlema  30885  lbslsat  31106  eulerpartlemb  31740  sgn3da  31913  fisshasheq  32466  hashfundm  32468  cvmsdisj  32631  cvmlift2lem12  32675  satfrel  32728  satfrnmapom  32731  fmlasuc  32747  satffun  32770  satef  32777  sategoelfv  32781  poseq  33209  frrlem12  33248  nosepon  33286  nolesgn2o  33292  nosepnelem  33298  nosepne  33299  nosepdmlem  33301  nosepdm  33302  nodenselem8  33309  noresle  33314  noetalem3  33333  sslttr  33382  scutbdaylt  33390  lineintmo  33732  nn0prpwlem  33784  nn0prpw  33785  neibastop2lem  33822  lindsadd  35049  areacirc  35149  incsequz  35185  mettrifi  35194  ismtybnd  35244  heiborlem1  35248  rngoisocnv  35418  risci  35424  eqvrelqsel  36010  lfl1  36365  lkrlsp2  36398  omlfh3N  36554  cvrnbtwn  36566  cvrnbtwn2  36570  cvrnbtwn4  36574  cvlexch3  36627  cvlexch4N  36628  cvlatexchb1  36629  2llnne2N  36703  atcvrj0  36723  cvrat2  36724  ps-1  36772  3atlem5  36782  islln2a  36812  lplnriaN  36845  lplnribN  36846  llncvrlpln2  36852  lplncvrlvol2  36910  psubatN  37050  pmapglb2N  37066  pmapglb2xN  37067  2llnma1b  37081  paddasslem17  37131  pmod2iN  37144  pmodl42N  37146  hlmod1i  37151  atmod1i1  37152  atmod1i2  37154  llnmod1i2  37155  pclcmpatN  37196  osumcllem8N  37258  pexmidlem3N  37267  pl42lem4N  37277  4atexlem7  37370  ltrnnid  37431  cdlemc4  37489  cdleme32a  37736  cdlemeg46gfre  37827  cdlemf2  37857  cdlemg4c  37907  trlcoat  38018  tendovalco  38060  tendoeq2  38069  cdlemk36  38208  diael  38338  diatrl  38339  dicelval1stN  38483  dicelval2nd  38484  dihlspsnat  38628  dochkr1  38773  lcfrlem9  38845  mapdh8e  39079  hdmapval0  39128  hgmapval0  39187  nnadddir  39464  nn0rppwr  39483  nn0expgcd  39485  incssnn0  39645  pell14qrexpcl  39801  pell14qrgap  39809  congadd  39900  acongsym  39910  acongtr  39912  dvdsacongtr  39918  jm2.19lem3  39925  jm2.19lem4  39926  jm2.26lem3  39935  bi13impia  41187  3impcombi  41516  ioogtlb  42125  iocgtlb  42132  iocleub  42133  icoltub  42138  iooltub  42140  limclner  42286  limsupre3lem  42367  climuzlem  42378  elfzelfzlble  43871  subsubelfzo0  43876  iccpartigtl  43933  sqrtpwpw2p  44048  fmtnoprmfac1lem  44074  fmtno4prmfac  44082  evenltle  44228  even3prm2  44230  wtgoldbnnsum4prm  44313  bgoldbnnsum3prm  44315  bgoldbtbndlem1  44316  bgoldbtbndlem3  44318  bgoldbtbndlem4  44319  bgoldbtbnd  44320  upgrwlkupwlk  44361  c0snmgmhm  44531  funcringcsetcALTV2lem9  44661  funcringcsetclem9ALTV  44684  lincscmcl  44834  lindslinindimp2lem4  44863  lincresunit2  44880  lincresunit3  44883  elfzolborelfzop1  44921  m1modmmod  44928  rege1logbzge0  44966  fllog2  44975  dignn0ldlem  45009  rrx2pnecoorneor  45122  rrx2plord2  45129  rrx2linest  45149
  Copyright terms: Public domain W3C validator