Theorem 3expa 1230

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

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

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 1007

This theorem is referenced by:  ad4ant123  1242  ad4ant124  1243  ad4ant134  1244  ad4ant234  1245  ad5ant123  1266  3anidm23  1334  mp3an2  1362  mpd3an3  1375  rgen3  2631  moi2  3001  sbc3ie  3119  2if2dc  3666  preq12bg  3882  issod  4445  wepo  4485  reuhypd  4597  funimass4  5732  fvtp1g  5897  f1imass  5953  fcof1o  5968  f1ofveu  6046  f1ocnvfv3  6047  acexmid  6057  2ndrn  6390  funsssuppss  6471  frecrdg  6652  oawordriexmid  6716  mapxpen  7114  findcard  7158  findcard2  7159  findcard2s  7160  ltapig  7669  ltanqi  7733  ltmnqi  7734  lt2addnq  7735  lt2mulnq  7736  prarloclemcalc  7833  genpassl  7855  genpassu  7856  prmuloc  7897  ltexprlemm  7931  ltexprlemfl  7940  ltexprlemfu  7942  lteupri  7948  ltaprg  7950  mul4  8421  add4  8450  cnegexlem2  8465  cnegexlem3  8466  2addsub  8503  addsubeq4  8504  muladd  8674  ltleadd  8737  reapmul1  8886  apreim  8894  receuap  8960  p1le  9140  lemul12b  9152  lbinf  9239  zdiv  9684  fzind  9711  fnn0ind  9712  uzss  9893  qmulcl  9987  qreccl  9992  xrlttr  10147  xaddass  10221  icc0r  10278  iooshf  10304  elfz5  10370  elfz0fzfz0  10482  fzind2  10607  ioo0  10643  ico0  10645  ioc0  10646  expnegap0  10933  expineg2  10934  mulexpzap  10965  expsubap  10973  expnbnd  11050  facndiv  11126  bccmpl  11141  bcval5  11150  bcpasc  11153  ccatrn  11322  swrdspsleq  11384  swrdccat2  11388  ccatpfx  11418  pfxccat1  11419  swrdswrd  11422  cats1un  11438  crim  11568  climshftlemg  12012  2sumeq2dv  12081  hash2iun  12190  2cprodeq2dv  12279  dvdsval3  12502  dvdsnegb  12519  muldvds1  12527  muldvds2  12528  dvdscmul  12529  dvdsmulc  12530  dvds2ln  12535  divalgb  12636  ndvdssub  12641  gcddiv  12740  rpexp1i  12876  phiprmpw  12944  hashgcdeq  12962  pythagtriplem1  12988  pockthg  13080  infpnlem1  13082  4sqlem3  13113  imasaddfnlemg  13578  mndpfo  13699  grplmulf1o  13829  grplactcnv  13857  mulgnn0subcl  13888  mulgsubcl  13889  mulgdir  13907  issubg2m  13942  issubgrpd2  13943  nmzsubg  13963  eqgen  13980  ghmmulg  14009  ghmf1  14026  kerf1ghm  14027  conjghm  14029  srglmhm  14236  srgrmhm  14237  ringlghm  14304  ringrghm  14305  oppr1g  14326  dvdsrcl2  14344  crngunit  14356  subsubrng  14460  subrgugrp  14486  subsubrg  14491  islmod  14565  lmodvsdir  14586  lmodvsass  14587  lsssubg  14651  lss1d  14657  lidlsubg  14760  lidlsubcl  14761  expghmap  14881  mulgghm2  14882  innei  15154  iscnp4  15209  cnpnei  15210  cnnei  15223  cnconst  15225  ismeti  15337  isxmet2d  15339  elbl2ps  15383  elbl2  15384  xblpnfps  15389  xblpnf  15390  xblm  15408  blininf  15415  blssexps  15420  blssex  15421  blsscls2  15484  metss  15485  metrest  15497  metcn  15505  divcnap  15556  cdivcncfap  15595  dvply1  15756  lgslem4  16002  lgscllem  16006  lgsneg1  16024  lgsne0  16037  uspgr2wlkeq  16486  eupth2lem3lem7fi  16595