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  3804  issod  4355  wepo  4395  reuhypd  4507  funimass4  5612  fvtp1g  5771  f1imass  5822  fcof1o  5837  f1ofveu  5911  f1ocnvfv3  5912  acexmid  5922  2ndrn  6242  frecrdg  6467  oawordriexmid  6529  mapxpen  6910  findcard  6950  findcard2  6951  findcard2s  6952  ltapig  7407  ltanqi  7471  ltmnqi  7472  lt2addnq  7473  lt2mulnq  7474  prarloclemcalc  7571  genpassl  7593  genpassu  7594  prmuloc  7635  ltexprlemm  7669  ltexprlemfl  7678  ltexprlemfu  7680  lteupri  7686  ltaprg  7688  mul4  8160  add4  8189  cnegexlem2  8204  cnegexlem3  8205  2addsub  8242  addsubeq4  8243  muladd  8412  ltleadd  8475  reapmul1  8624  apreim  8632  receuap  8698  p1le  8878  lemul12b  8890  lbinf  8977  zdiv  9416  fzind  9443  fnn0ind  9444  uzss  9624  qmulcl  9713  qreccl  9718  xrlttr  9872  xaddass  9946  icc0r  10003  iooshf  10029  elfz5  10094  elfz0fzfz0  10203  fzind2  10317  ioo0  10351  ico0  10353  ioc0  10354  expnegap0  10641  expineg2  10642  mulexpzap  10673  expsubap  10681  expnbnd  10757  facndiv  10833  bccmpl  10848  bcval5  10857  bcpasc  10860  crim  11025  climshftlemg  11469  2sumeq2dv  11538  hash2iun  11646  2cprodeq2dv  11735  dvdsval3  11958  dvdsnegb  11975  muldvds1  11983  muldvds2  11984  dvdscmul  11985  dvdsmulc  11986  dvds2ln  11991  divalgb  12092  ndvdssub  12097  gcddiv  12196  rpexp1i  12332  phiprmpw  12400  hashgcdeq  12418  pythagtriplem1  12444  pockthg  12536  infpnlem1  12538  4sqlem3  12569  imasaddfnlemg  12967  mndpfo  13089  grplmulf1o  13216  grplactcnv  13244  mulgnn0subcl  13275  mulgsubcl  13276  mulgdir  13294  issubg2m  13329  issubgrpd2  13330  nmzsubg  13350  eqgen  13367  ghmmulg  13396  ghmf1  13413  kerf1ghm  13414  conjghm  13416  srglmhm  13559  srgrmhm  13560  ringlghm  13627  ringrghm  13628  oppr1g  13648  dvdsrcl2  13665  crngunit  13677  subsubrng  13780  subrgugrp  13806  subsubrg  13811  islmod  13857  lmodvsdir  13878  lmodvsass  13879  lsssubg  13943  lss1d  13949  lidlsubg  14052  lidlsubcl  14053  expghmap  14173  mulgghm2  14174  innei  14409  iscnp4  14464  cnpnei  14465  cnnei  14478  cnconst  14480  ismeti  14592  isxmet2d  14594  elbl2ps  14638  elbl2  14639  xblpnfps  14644  xblpnf  14645  xblm  14663  blininf  14670  blssexps  14675  blssex  14676  blsscls2  14739  metss  14740  metrest  14752  metcn  14760  divcnap  14811  cdivcncfap  14850  dvply1  15011  lgslem4  15254  lgscllem  15258  lgsneg1  15276  lgsne0  15289