Theorem 3expa 1234

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

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   /\ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  ad4ant123  1246  ad4ant124  1247  ad4ant134  1248  ad4ant234  1249  ad5ant123  1270  3anidm23  1338  mp3an2  1366  mpd3an3  1379  rgen3  2637  moi2  3007  sbc3ie  3125  2if2dc  3680  preq12bg  3898  issod  4464  wepo  4504  reuhypd  4617  funimass4  5753  fvtp1g  5923  f1imass  5980  fcof1o  5995  f1ofveu  6073  f1ocnvfv3  6074  acexmid  6084  2ndrn  6417  funsssuppss  6498  frecrdg  6679  oawordriexmid  6743  mapxpen  7148  findcard  7192  findcard2  7193  findcard2s  7194  ltapig  7705  ltanqi  7769  ltmnqi  7770  lt2addnq  7771  lt2mulnq  7772  prarloclemcalc  7869  genpassl  7891  genpassu  7892  prmuloc  7933  ltexprlemm  7967  ltexprlemfl  7976  ltexprlemfu  7978  lteupri  7984  ltaprg  7986  mul4  8458  add4  8487  cnegexlem2  8502  cnegexlem3  8503  2addsub  8540  addsubeq4  8541  muladd  8711  ltleadd  8774  reapmul1  8923  apreim  8931  receuap  8999  p1le  9179  lemul12b  9191  lbinf  9278  zdiv  9734  fzind  9761  fnn0ind  9762  uzss  9943  qmulcl  10037  qreccl  10042  xrlttr  10197  xaddass  10271  icc0r  10328  iooshf  10354  elfz5  10420  elfz0fzfz0  10533  fzind2  10658  ioo0  10694  ico0  10696  ioc0  10697  expnegap0  10984  expineg2  10985  mulexpzap  11016  expsubap  11024  expnbnd  11101  facndiv  11177  bccmpl  11192  bcval5  11201  bcpasc  11204  ccatrn  11377  swrdspsleq  11439  swrdccat2  11443  ccatpfx  11473  pfxccat1  11474  swrdswrd  11477  cats1un  11493  crim  11623  climshftlemg  12068  2sumeq2dv  12137  hash2iun  12246  2cprodeq2dv  12335  dvdsval3  12558  dvdsnegb  12575  muldvds1  12583  muldvds2  12584  dvdscmul  12585  dvdsmulc  12586  dvds2ln  12591  divalgb  12692  ndvdssub  12697  gcddiv  12796  rpexp1i  12932  phiprmpw  13000  hashgcdeq  13018  pythagtriplem1  13044  pockthg  13136  infpnlem1  13138  4sqlem3  13169  imasaddfnlemg  13635  mndpfo  13751  grplmulf1o  13879  grplactcnv  13907  mulgnn0subcl  13938  mulgsubcl  13939  mulgdir  13957  issubg2m  13992  issubgrpd2  13993  nmzsubg  14013  eqgen  14030  ghmmulg  14059  ghmf1  14076  kerf1ghm  14077  conjghm  14079  srglmhm  14297  srgrmhm  14298  ringlghm  14366  ringrghm  14367  oppr1g  14388  dvdsrcl2  14406  crngunit  14418  subsubrng  14522  subrgugrp  14548  subsubrg  14553  islmod  14627  lmodvsdir  14649  lmodvsass  14650  lsssubg  14714  lss1d  14720  lidlsubg  14823  lidlsubcl  14824  expghmap  14942  mulgghm2  14943  innei  15264  iscnp4  15319  cnpnei  15320  cnnei  15333  cnconst  15335  ismeti  15447  isxmet2d  15449  elbl2ps  15493  elbl2  15494  xblpnfps  15499  xblpnf  15500  xblm  15518  blininf  15525  blssexps  15530  blssex  15531  blsscls2  15594  metss  15595  metrest  15607  metcn  15615  divcnap  15666  cdivcncfap  15705  dvply1  15866  lgslem4  16122  lgscllem  16126  lgsneg1  16144  lgsne0  16157  uspgr2wlkeq  16606  eupth2lem3lem7fi  16715