Theorem 3impb 1260

Description: Importation from double to triple conjunction. (Contributed by NM, 20-Aug-1995.)

Hypothesis

Ref	Expression
3impb.1	|- ( ( ph /\ ( ps /\ ch ) ) -> th )

Assertion

Ref	Expression
3impb	|- ( ( ph /\ ps /\ ch ) -> th )

Proof of Theorem 3impb

Step	Hyp	Ref	Expression
1		3impb.1	. . 3 |- ( ( ph /\ ( ps /\ ch ) ) -> th )
2	1	exp32 631	. 2 |- ( ph -> ( ps -> ( ch -> th ) ) )
3	2	3imp 1256	1 |- ( ( ph /\ ps /\ ch ) -> th )

Syntax hints:   -> wi 4   /\ wa 384   /\ w3a 1037

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 1039

This theorem is referenced by:  3adant1l  1318  3adant1r  1319  3impdi  1381  rsp2e  3004  vtocl3gf  3269  rspc2ev  3324  reuss  3908  frc  5080  trssord  5740  funtp  5945  resdif  6157  fnotovb  6694  fovrn  6804  fnovrn  6809  fmpt2co  7260  smoord  7462  odi  7659  oeoa  7677  oeoe  7679  nndi  7703  ecopovtrn  7850  ecovass  7855  ecovdi  7856  suppr  8377  infpr  8409  harval2  8823  cdaassen  9004  fin23lem31  9165  tskuni  9605  addasspi  9717  mulasspi  9719  distrpi  9720  mulcanenq  9782  genpass  9831  distrlem1pr  9847  prlem934  9855  ltapr  9867  le2tri3i  10167  subadd  10284  addsub  10292  subdi  10463  submul2  10470  ltaddsub  10502  leaddsub  10504  divval  10687  div12  10707  diveq1  10718  divneg  10719  divdiv2  10737  ltmulgt11  10883  gt0div  10889  ge0div  10890  uzind3  11471  fnn0ind  11476  qdivcl  11809  irrmul  11813  xrlttr  11973  fzen  12358  modcyc  12705  modcyc2  12706  faclbnd4lem4  13083  cshweqdifid  13566  lenegsq  14060  moddvds  14991  dvdscmulr  15010  dvdsmulcr  15011  dvds2add  15015  dvds2sub  15016  dvdsleabs  15033  divalg  15126  divalgb  15127  ndvdsadd  15134  gcdcllem3  15223  dvdslegcd  15226  modgcd  15253  absmulgcd  15266  odzval  15496  pcmul  15556  ressid2  15928  ressval2  15929  catcisolem  16756  prf1st  16844  prf2nd  16845  1st2ndprf  16846  curfuncf  16878  curf2ndf  16887  pltval  16960  pospo  16973  lubel  17122  isdlat  17193  issubmnd  17318  prdsmndd  17323  submcl  17353  grpinvid1  17470  grpinvid2  17471  mulgp1  17574  ghmlin  17665  ghmsub  17668  odlem2  17958  gexlem2  17997  lsmvalx  18054  efgtval  18136  cmncom  18209  lssvnegcl  18956  islss3  18959  prdslmodd  18969  evlslem2  19512  evlseu  19516  zntoslem  19905  maducoeval2  20446  madutpos  20448  madugsum  20449  madurid  20450  m2cpminvid  20558  pm2mpghm  20621  unopn  20708  ntrss  20859  innei  20929  t1sep2  21173  metustsym  22360  cncfi  22697  rrxds  23181  quotval  24047  abelthlem2  24186  mudivsum  25219  padicabv  25319  axsegconlem1  25797  nsnlplig  27333  nsnlpligALT  27334  grpoinvid1  27382  grpoinvid2  27383  grpodivval  27389  ablo4  27404  ablonncan  27411  nvnpcan  27511  nvmeq0  27513  nvabs  27527  imsdval  27541  ipval  27558  nmorepnf  27623  blo3i  27657  blometi  27658  ipasslem5  27690  hvmulcan  27929  his5  27943  his7  27947  his2sub2  27950  hhssabloilem  28118  hhssnv  28121  fh1  28477  fh2  28478  cm2j  28479  homcl  28605  homco1  28660  homulass  28661  hoadddi  28662  hosubsub2  28671  braadd  28804  bramul  28805  lnopmul  28826  lnopli  28827  lnopaddmuli  28832  lnopsubmuli  28834  lnfnli  28899  lnfnaddmuli  28904  kbass2  28976  mdexchi  29194  xdivval  29627  resvid2  29828  resvval2  29829  unitdivcld  29947  bnj229  30954  bnj546  30966  bnj570  30975  cvmlift2lem7  31291  nosupfv  31852  nosupres  31853  finminlem  32312  ivthALT  32330  topdifinffinlem  33195  exidcl  33675  grposnOLD  33681  rngoneglmul  33742  rngonegrmul  33743  divrngcl  33756  crngocom  33800  crngm4  33802  inidl  33829  oposlem  34469  hlsuprexch  34667  ldilcnv  35401  ltrnu  35407  tgrpgrplem  36037  tgrpabl  36039  erngdvlem3  36278  erngdvlem3-rN  36286  dvalveclem  36314  dvhfvadd  36380  dvhgrp  36396  dvhlveclem  36397  djhval2  36688  diophren  37377  monotoddzzfi  37507  rpexpmord  37513  ltrmynn0  37515  ltrmxnn0  37516  lermxnn0  37517  rmyeq  37521  lermy  37522  jm2.21  37561  radcnvrat  38513  dvconstbi  38533  expgrowth  38534  bi3impb  38689  eel132  38927  xlimmnfvlem2  40059  xlimpnfvlem2  40063  fnotaovb  41278  ccatpfx  41409  submgmcl  41794  onetansqsecsq  42502