Theorem 3expa 1205

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

Hypothesis

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

Assertion

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

Proof of Theorem 3expa

Step	Hyp	Ref	Expression
1		3exp.1	. . 3 |- ( ( ph /\ ps /\ ch ) -> th )
2	1	3exp 1204	. 2 |- ( ph -> ( ps -> ( ch -> th ) ) )
3	2	imp31 256	1 |- ( ( ( ph /\ ps ) /\ ch ) -> th )

Syntax hints:   -> wi 4   /\ wa 104   /\ w3a 980

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117  df-3an 982

This theorem is referenced by:  ad4ant123  1217  ad4ant124  1218  ad4ant134  1219  ad4ant234  1220  ad5ant123  1241  3anidm23  1308  mp3an2  1336  mpd3an3  1349  rgen3  2584  moi2  2945  sbc3ie  3063  preq12bg  3803  issod  4354  wepo  4394  reuhypd  4506  funimass4  5611  fvtp1g  5770  f1imass  5821  fcof1o  5836  f1ofveu  5910  f1ocnvfv3  5911  acexmid  5921  2ndrn  6241  frecrdg  6466  oawordriexmid  6528  mapxpen  6909  findcard  6949  findcard2  6950  findcard2s  6951  ltapig  7405  ltanqi  7469  ltmnqi  7470  lt2addnq  7471  lt2mulnq  7472  prarloclemcalc  7569  genpassl  7591  genpassu  7592  prmuloc  7633  ltexprlemm  7667  ltexprlemfl  7676  ltexprlemfu  7678  lteupri  7684  ltaprg  7686  mul4  8158  add4  8187  cnegexlem2  8202  cnegexlem3  8203  2addsub  8240  addsubeq4  8241  muladd  8410  ltleadd  8473  reapmul1  8622  apreim  8630  receuap  8696  p1le  8876  lemul12b  8888  lbinf  8975  zdiv  9414  fzind  9441  fnn0ind  9442  uzss  9622  qmulcl  9711  qreccl  9716  xrlttr  9870  xaddass  9944  icc0r  10001  iooshf  10027  elfz5  10092  elfz0fzfz0  10201  fzind2  10315  ioo0  10349  ico0  10351  ioc0  10352  expnegap0  10639  expineg2  10640  mulexpzap  10671  expsubap  10679  expnbnd  10755  facndiv  10831  bccmpl  10846  bcval5  10855  bcpasc  10858  crim  11023  climshftlemg  11467  2sumeq2dv  11536  hash2iun  11644  2cprodeq2dv  11733  dvdsval3  11956  dvdsnegb  11973  muldvds1  11981  muldvds2  11982  dvdscmul  11983  dvdsmulc  11984  dvds2ln  11989  divalgb  12090  ndvdssub  12095  gcddiv  12186  rpexp1i  12322  phiprmpw  12390  hashgcdeq  12408  pythagtriplem1  12434  pockthg  12526  infpnlem1  12528  4sqlem3  12559  imasaddfnlemg  12957  mndpfo  13079  grplmulf1o  13206  grplactcnv  13234  mulgnn0subcl  13265  mulgsubcl  13266  mulgdir  13284  issubg2m  13319  issubgrpd2  13320  nmzsubg  13340  eqgen  13357  ghmmulg  13386  ghmf1  13403  kerf1ghm  13404  conjghm  13406  srglmhm  13549  srgrmhm  13550  ringlghm  13617  ringrghm  13618  oppr1g  13638  dvdsrcl2  13655  crngunit  13667  subsubrng  13770  subrgugrp  13796  subsubrg  13801  islmod  13847  lmodvsdir  13868  lmodvsass  13869  lsssubg  13933  lss1d  13939  lidlsubg  14042  lidlsubcl  14043  expghmap  14163  mulgghm2  14164  innei  14399  iscnp4  14454  cnpnei  14455  cnnei  14468  cnconst  14470  ismeti  14582  isxmet2d  14584  elbl2ps  14628  elbl2  14629  xblpnfps  14634  xblpnf  14635  xblm  14653  blininf  14660  blssexps  14665  blssex  14666  blsscls2  14729  metss  14730  metrest  14742  metcn  14750  divcnap  14801  cdivcncfap  14840  dvply1  15001  lgslem4  15244  lgscllem  15248  lgsneg1  15266  lgsne0  15279