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

Theorem 3impb 1143
Description: Importation from double to triple conjunction. (Contributed by NM, 20-Aug-1995.)
Hypothesis
Ref Expression
3impb.1 ((𝜑 ∧ (𝜓𝜒)) → 𝜃)
Assertion
Ref Expression
3impb ((𝜑𝜓𝜒) → 𝜃)

Proof of Theorem 3impb
StepHypRef Expression
1 3impb.1 . . 3 ((𝜑 ∧ (𝜓𝜒)) → 𝜃)
21exp32 411 . 2 (𝜑 → (𝜓 → (𝜒𝜃)))
323imp 1137 1 ((𝜑𝜓𝜒) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  w3a 1107
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 198  df-an 385  df-3an 1109
This theorem is referenced by:  3adant3  1162  3adant1lOLD  1222  3adant1rOLD  1224  3impdi  1459  rsp2e  3150  vtocl3gf  3421  rspc2ev  3476  reuss  4072  frc  5243  trssord  5925  funtp  6124  resdif  6340  fnotovb  6891  fnotovbOLD  6892  fovrn  7002  fnovrn  7007  fmpt2co  7462  smoord  7666  odi  7864  oeoa  7882  oeoe  7884  nndi  7908  ecopovtrn  8054  ecovass  8058  ecovdi  8059  suppr  8584  infpr  8616  harval2  9074  cdaassen  9257  fin23lem31  9418  tskuni  9858  addasspi  9970  mulasspi  9972  distrpi  9973  mulcanenq  10035  genpass  10084  distrlem1pr  10100  prlem934  10108  ltapr  10120  le2tri3i  10421  subadd  10538  addsub  10546  subdi  10717  submul2  10724  ltaddsub  10756  leaddsub  10758  divval  10941  div12  10961  diveq1  10972  divneg  10973  divdiv2  10991  ltmulgt11  11137  gt0div  11143  ge0div  11144  uzind3  11718  fnn0ind  11723  qdivcl  12010  irrmul  12014  xrlttr  12173  fzen  12565  modcyc  12913  modcyc2  12914  faclbnd4lem4  13287  ccatval21sw  13556  ccatpfx  13688  cshweqdifid  13849  lenegsq  14345  moddvds  15276  dvdscmulr  15295  dvdsmulcr  15296  dvds2add  15300  dvds2sub  15301  dvdsleabs  15318  divalg  15408  divalgb  15409  ndvdsadd  15415  gcdcllem3  15504  dvdslegcd  15507  modgcd  15534  absmulgcd  15547  odzval  15775  pcmul  15835  ressid2  16200  ressval2  16201  catcisolem  17021  prf1st  17110  prf2nd  17111  1st2ndprf  17112  curfuncf  17144  curf2ndf  17153  pltval  17226  pospo  17239  lubel  17388  isdlat  17459  issubmnd  17584  prdsmndd  17589  submcl  17619  grpinvid1  17737  grpinvid2  17738  mulgp1  17839  ghmlin  17929  ghmsub  17932  odlem2  18222  gexlem2  18261  lsmvalx  18318  efgtval  18400  cmncom  18475  lssvnegcl  19228  islss3  19231  prdslmodd  19241  evlslem2  19785  evlseu  19789  zntoslem  20177  maducoeval2  20723  madutpos  20725  madugsum  20726  madurid  20727  m2cpminvid  20837  pm2mpghm  20900  unopn  20987  ntrss  21139  innei  21209  t1sep2  21453  metustsym  22639  cncfi  22976  rrxds  23470  quotval  24338  abelthlem2  24477  mudivsum  25510  padicabv  25610  axsegconlem1  26088  nsnlplig  27792  nsnlpligALT  27793  grpoinvid1  27839  grpoinvid2  27840  grpodivval  27846  ablo4  27861  ablonncan  27867  nvnpcan  27967  nvmeq0  27969  nvabs  27983  imsdval  27997  ipval  28014  nmorepnf  28079  blo3i  28113  blometi  28114  ipasslem5  28146  hvmulcan  28385  his5  28399  his7  28403  his2sub2  28406  hhssabloilem  28574  hhssnv  28577  fh1  28933  fh2  28934  cm2j  28935  homcl  29061  homco1  29116  homulass  29117  hoadddi  29118  hosubsub2  29127  braadd  29260  bramul  29261  lnopmul  29282  lnopli  29283  lnopaddmuli  29288  lnopsubmuli  29290  lnfnli  29355  lnfnaddmuli  29360  kbass2  29432  mdexchi  29650  xdivval  30074  resvid2  30275  resvval2  30276  unitdivcld  30394  bnj229  31402  bnj546  31414  bnj570  31423  cvmlift2lem7  31739  nosupfv  32296  nosupres  32297  finminlem  32756  ivthALT  32773  topdifinffinlem  33628  exidcl  34097  grposnOLD  34103  rngoneglmul  34164  rngonegrmul  34165  divrngcl  34178  crngocom  34222  crngm4  34224  inidl  34251  xrninxpex  34581  oposlem  35138  hlsuprexch  35337  ldilcnv  36071  ltrnu  36077  tgrpgrplem  36705  tgrpabl  36707  erngdvlem3  36946  erngdvlem3-rN  36954  dvalveclem  36981  dvhfvadd  37047  dvhgrp  37063  dvhlveclem  37064  djhval2  37355  diophren  38055  monotoddzzfi  38184  rpexpmord  38190  ltrmynn0  38192  ltrmxnn0  38193  lermxnn0  38194  rmyeq  38198  lermy  38199  jm2.21  38238  radcnvrat  39187  dvconstbi  39207  expgrowth  39208  bi3impb  39361  eel132  39589  xlimmnfvlem2  40697  xlimpnfvlem2  40701  fnotaovb  41946  submgmcl  42463  onetansqsecsq  43174
  Copyright terms: Public domain W3C validator