Theorem 3expa 1206

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 1205	. 2 |- ( ph -> ( ps -> ( ch -> th ) ) )
3	2	imp31 256	1 |- ( ( ( ph /\ ps ) /\ ch ) -> th )

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

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 983

This theorem is referenced by:  ad4ant123  1218  ad4ant124  1219  ad4ant134  1220  ad4ant234  1221  ad5ant123  1242  3anidm23  1310  mp3an2  1338  mpd3an3  1351  rgen3  2593  moi2  2954  sbc3ie  3072  preq12bg  3814  issod  4367  wepo  4407  reuhypd  4519  funimass4  5631  fvtp1g  5794  f1imass  5845  fcof1o  5860  f1ofveu  5934  f1ocnvfv3  5935  acexmid  5945  2ndrn  6271  frecrdg  6496  oawordriexmid  6558  mapxpen  6947  findcard  6987  findcard2  6988  findcard2s  6989  ltapig  7453  ltanqi  7517  ltmnqi  7518  lt2addnq  7519  lt2mulnq  7520  prarloclemcalc  7617  genpassl  7639  genpassu  7640  prmuloc  7681  ltexprlemm  7715  ltexprlemfl  7724  ltexprlemfu  7726  lteupri  7732  ltaprg  7734  mul4  8206  add4  8235  cnegexlem2  8250  cnegexlem3  8251  2addsub  8288  addsubeq4  8289  muladd  8458  ltleadd  8521  reapmul1  8670  apreim  8678  receuap  8744  p1le  8924  lemul12b  8936  lbinf  9023  zdiv  9463  fzind  9490  fnn0ind  9491  uzss  9671  qmulcl  9760  qreccl  9765  xrlttr  9919  xaddass  9993  icc0r  10050  iooshf  10076  elfz5  10141  elfz0fzfz0  10250  fzind2  10370  ioo0  10404  ico0  10406  ioc0  10407  expnegap0  10694  expineg2  10695  mulexpzap  10726  expsubap  10734  expnbnd  10810  facndiv  10886  bccmpl  10901  bcval5  10910  bcpasc  10913  ccatrn  11068  swrdspsleq  11123  swrdccat2  11127  ccatpfx  11155  pfxccat1  11156  crim  11202  climshftlemg  11646  2sumeq2dv  11715  hash2iun  11823  2cprodeq2dv  11912  dvdsval3  12135  dvdsnegb  12152  muldvds1  12160  muldvds2  12161  dvdscmul  12162  dvdsmulc  12163  dvds2ln  12168  divalgb  12269  ndvdssub  12274  gcddiv  12373  rpexp1i  12509  phiprmpw  12577  hashgcdeq  12595  pythagtriplem1  12621  pockthg  12713  infpnlem1  12715  4sqlem3  12746  imasaddfnlemg  13179  mndpfo  13303  grplmulf1o  13439  grplactcnv  13467  mulgnn0subcl  13504  mulgsubcl  13505  mulgdir  13523  issubg2m  13558  issubgrpd2  13559  nmzsubg  13579  eqgen  13596  ghmmulg  13625  ghmf1  13642  kerf1ghm  13643  conjghm  13645  srglmhm  13788  srgrmhm  13789  ringlghm  13856  ringrghm  13857  oppr1g  13877  dvdsrcl2  13894  crngunit  13906  subsubrng  14009  subrgugrp  14035  subsubrg  14040  islmod  14086  lmodvsdir  14107  lmodvsass  14108  lsssubg  14172  lss1d  14178  lidlsubg  14281  lidlsubcl  14282  expghmap  14402  mulgghm2  14403  innei  14668  iscnp4  14723  cnpnei  14724  cnnei  14737  cnconst  14739  ismeti  14851  isxmet2d  14853  elbl2ps  14897  elbl2  14898  xblpnfps  14903  xblpnf  14904  xblm  14922  blininf  14929  blssexps  14934  blssex  14935  blsscls2  14998  metss  14999  metrest  15011  metcn  15019  divcnap  15070  cdivcncfap  15109  dvply1  15270  lgslem4  15513  lgscllem  15517  lgsneg1  15535  lgsne0  15548