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

Theorem 3impb 1252
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 629 . 2 (𝜑 → (𝜓 → (𝜒𝜃)))
323imp 1249 1 ((𝜑𝜓𝜒) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  w3a 1031
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 196  df-an 385  df-3an 1033
This theorem is referenced by:  3adant1l  1310  3adant1r  1311  3impdi  1373  rsp2e  2987  vtocl3gf  3242  rspc2ev  3295  reuss  3867  frc  5004  trssord  5657  funtp  5859  resdif  6070  fnotovb  6592  fovrn  6702  fnovrn  6707  fmpt2co  7147  smoord  7349  odi  7546  oeoa  7564  oeoe  7566  nndi  7590  ecopovtrn  7737  ecovass  7742  ecovdi  7743  suppr  8260  infpr  8292  harval2  8706  cdaassen  8887  fin23lem31  9048  tskuni  9484  addasspi  9596  mulasspi  9598  distrpi  9599  mulcanenq  9661  genpass  9710  distrlem1pr  9726  prlem934  9734  ltapr  9746  le2tri3i  10046  subadd  10163  addsub  10171  subdi  10342  submul2  10349  ltaddsub  10381  leaddsub  10383  divval  10566  div12  10586  diveq1  10597  divneg  10598  divdiv2  10616  ltmulgt11  10762  gt0div  10768  ge0div  10769  uzind3  11347  fnn0ind  11352  qdivcl  11685  irrmul  11689  xrlttr  11849  fzen  12229  modcyc  12567  modcyc2  12568  faclbnd4lem4  12945  cshweqdifid  13417  lenegsq  13908  moddvds  14829  dvdscmulr  14848  dvdsmulcr  14849  dvds2add  14853  dvds2sub  14854  dvdsleabs  14871  divalg  14964  divalgb  14965  ndvdsadd  14972  gcdcllem3  15061  dvdslegcd  15064  modgcd  15091  absmulgcd  15104  odzval  15334  pcmul  15394  ressid2  15755  ressval2  15756  catcisolem  16579  prf1st  16667  prf2nd  16668  1st2ndprf  16669  curfuncf  16701  curf2ndf  16710  pltval  16783  pospo  16796  lubel  16945  isdlat  17016  issubmnd  17141  prdsmndd  17146  submcl  17176  grpinvid1  17293  grpinvid2  17294  mulgp1  17397  ghmlin  17488  ghmsub  17491  odlem2  17781  gexlem2  17820  lsmvalx  17877  efgtval  17959  cmncom  18032  lssvnegcl  18777  islss3  18780  prdslmodd  18790  evlslem2  19333  evlseu  19337  zntoslem  19724  maducoeval2  20265  madutpos  20267  madugsum  20268  madurid  20269  m2cpminvid  20377  pm2mpghm  20440  unopn  20533  ntrss  20669  innei  20739  t1sep2  20983  metustsym  22170  cncfi  22505  rrxds  22989  quotval  23851  abelthlem2  23990  mudivsum  25019  padicabv  25119  axsegconlem1  25597  frgregordn0  26597  grpoinvid1  26766  grpoinvid2  26767  grpodivval  26773  ablo4  26788  ablonncan  26795  nvnpcan  26895  nvmeq0  26897  nvabs  26911  imsdval  26925  ipval  26942  nmorepnf  27007  blo3i  27041  blometi  27042  ipasslem5  27074  hvmulcan  27313  his5  27327  his7  27331  his2sub2  27334  hhssabloilem  27502  hhssnv  27505  fh1  27861  fh2  27862  cm2j  27863  homcl  27989  homco1  28044  homulass  28045  hoadddi  28046  hosubsub2  28055  braadd  28188  bramul  28189  lnopmul  28210  lnopli  28211  lnopaddmuli  28216  lnopsubmuli  28218  lnfnli  28283  lnfnaddmuli  28288  kbass2  28360  mdexchi  28578  xdivval  28958  resvid2  29159  resvval2  29160  unitdivcld  29275  bnj229  30208  bnj546  30220  bnj570  30229  cvmlift2lem7  30545  finminlem  31482  ivthALT  31500  topdifinffinlem  32371  exidcl  32845  grposnOLD  32851  rngoneglmul  32912  rngonegrmul  32913  divrngcl  32926  crngocom  32970  crngm4  32972  inidl  32999  oposlem  33487  hlsuprexch  33685  ldilcnv  34419  ltrnu  34425  tgrpgrplem  35055  tgrpabl  35057  erngdvlem3  35296  erngdvlem3-rN  35304  dvalveclem  35332  dvhfvadd  35398  dvhgrp  35414  dvhlveclem  35415  djhval2  35706  diophren  36395  monotoddzzfi  36525  rpexpmord  36531  ltrmynn0  36533  ltrmxnn0  36534  lermxnn0  36535  rmyeq  36539  lermy  36540  jm2.21  36579  radcnvrat  37535  dvconstbi  37555  expgrowth  37556  bi3impb  37710  eel132  37948  fnotaovb  39927  ccatpfx  40272  frgrhash2wsp  41497  submgmcl  41584  onetansqsecsq  42301
  Copyright terms: Public domain W3C validator