Theorem 3impa 1259

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

Hypothesis

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

Assertion

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

Proof of Theorem 3impa

Step	Hyp	Ref	Expression
1		3impa.1	. . 3 |- ( ( ( ph /\ ps ) /\ ch ) -> th )
2	1	exp31 630	. 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:  ex3  1263  3impdir  1382  syl3an9b  1397  biimp3a  1432  stoic3  1701  rspec3  2935  rspc3v  3325  raltpg  4236  rextpg  4237  disjiun  4640  otthg  4954  3optocl  5197  fun2ssres  5931  funtpg  5942  funssfv  6209  foco2OLD  6380  f1elima  6520  ot1stg  7182  ot2ndg  7183  smogt  7464  omord2  7647  omword  7650  oeword  7670  omabslem  7726  ecovass  7855  fpmg  7883  findcard  8199  cdaun  8994  cfsmolem  9092  ingru  9637  addasspi  9717  mulasspi  9719  ltapi  9725  ltmpi  9726  axpre-ltadd  9988  leltne  10127  dedekind  10200  recextlem2  10658  divdiv32  10733  divdiv1  10736  lble  10975  fnn0ind  11476  supminf  11775  xrleltne  11978  xrmaxeq  12010  xrmineq  12011  iccgelb  12230  elicc4  12240  iccsplit  12305  elfz  12332  fzrevral  12425  modabs  12703  expgt0  12893  expge0  12896  expge1  12897  mulexpz  12900  expp1z  12909  expm1  12910  digit1  12998  faclbnd4  13084  faclbnd5  13085  s3eqs2s1eq  13683  abssubne0  14056  binom  14562  dvds0lem  14992  dvdsnegb  14999  muldvds1  15006  muldvds2  15007  dvdscmulr  15010  dvdsmulcr  15011  divalgmodcl  15131  gcd2n0cl  15231  gcdaddm  15246  lcmdvds  15321  prmdvdsexp  15427  rpexp1i  15433  monpropd  16397  prfval  16839  xpcpropd  16848  curf2ndf  16887  eqglact  17645  mndodcongi  17962  oddvdsnn0  17963  efgi0  18133  efgi1  18134  lss0cl  18947  scmatscmid  20312  pmatcollpw3fi1lem1  20591  cnpval  21040  cnf2  21053  cnnei  21086  lfinun  21328  ptpjcn  21414  cnmptk2  21489  flfval  21794  cnmpt2plusg  21892  cnmpt2vsca  21998  ustincl  22011  xbln0  22219  blssec  22240  blpnfctr  22241  mopni2  22298  mopni3  22299  nmoval  22519  nmocl  22524  isnghm2  22528  isnmhm2  22556  cnmpt2ds  22646  metdseq0  22657  cnmpt2ip  23047  caucfil  23081  mbfimasn  23401  dvnf  23690  dvnbss  23691  coemul  24008  dvply1  24039  dvnply2  24042  pserdvlem2  24182  logeftb  24330  advlogexp  24401  cxpne0  24423  cxpp1  24426  lgsne0  25060  f1otrg  25751  ax5seglem9  25817  uhgrn0  25962  upgrn0  25984  upgrle  25985  uhgrwkspthlem2  26650  frgrhash2wsp  27196  sspval  27578  sspnval  27592  lnof  27610  nmooval  27618  nmooge0  27622  nmoub3i  27628  bloln  27639  nmblore  27641  hosval  28599  homval  28600  hodval  28601  hfsval  28602  hfmval  28603  homulass  28661  hoadddir  28663  nmopub2tALT  28768  nmfnleub2  28785  kbval  28813  lnopmul  28826  0lnfn  28844  lnopcoi  28862  nmcoplb  28889  nmcfnlb  28913  kbass2  28976  nmopleid  28998  hstoh  29091  mdi  29154  dmdi  29161  dmdi4  29166  supxrnemnf  29534  reofld  29840  bnj605  30977  bnj607  30986  bnj1097  31049  elno2  31807  topdifinffinlem  33195  lindsdom  33403  lindsenlbs  33404  ftc1anclem2  33486  fzmul  33537  nninfnub  33547  exidreslem  33676  grposnOLD  33681  ghomf  33689  rngohomf  33765  rngohom1  33767  rngohomadd  33768  rngohommul  33769  rngoiso1o  33778  rngoisohom  33779  igenmin  33863  lkrcl  34379  lkrf0  34380  omlfh1N  34545  tendoex  36263  3anrabdioph  37346  3orrabdioph  37347  rencldnfilem  37384  expmordi  37512  dvdsabsmod0  37554  jm2.18  37555  jm2.25  37566  jm2.15nn0  37570  addrfv  38673  subrfv  38674  mulvfv  38675  bi3impa  38690  ssfiunibd  39523  supminfxr  39694  limsupgtlem  40009  xlimmnfv  40060  xlimpnfv  40064  dvnmul  40158  stoweidlem34  40251  stoweidlem48  40265  sge0cl  40598  sge0xp  40646  ovnsubaddlem1  40784  ovnovollem3  40872  aovmpt4g  41281  gboge9  41652