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  4466  wepo  4506  reuhypd  4619  funimass4  5756  fvtp1g  5926  f1imass  5983  fcof1o  5998  f1ofveu  6076  f1ocnvfv3  6077  acexmid  6087  2ndrn  6421  funsssuppss  6502  frecrdg  6684  oawordriexmid  6748  mapxpen  7154  findcard  7198  findcard2  7199  findcard2s  7200  ltapig  7711  ltanqi  7775  ltmnqi  7776  lt2addnq  7777  lt2mulnq  7778  prarloclemcalc  7875  genpassl  7897  genpassu  7898  prmuloc  7939  ltexprlemm  7973  ltexprlemfl  7982  ltexprlemfu  7984  lteupri  7990  ltaprg  7992  mul4  8465  add4  8494  cnegexlem2  8509  cnegexlem3  8510  2addsub  8547  addsubeq4  8548  muladd  8718  ltleadd  8781  reapmul1  8931  apreim  8939  receuap  9007  p1le  9187  lemul12b  9199  lbinf  9286  zdiv  9744  fzind  9771  fnn0ind  9772  uzss  9958  qmulcl  10052  qreccl  10057  xrlttr  10213  xaddass  10287  icc0r  10344  iooshf  10370  elfz5  10436  elfz0fzfz0  10549  fzind2  10674  ioo0  10710  ico0  10712  ioc0  10713  expnegap0  11004  expineg2  11005  mulexpzap  11036  expsubap  11044  expnbnd  11121  facndiv  11198  bccmpl  11213  bcval5  11222  bcpasc  11225  ccatrn  11398  swrdspsleq  11460  swrdccat2  11464  ccatpfx  11494  pfxccat1  11495  swrdswrd  11498  cats1un  11514  crim  11644  climshftlemg  12092  2sumeq2dv  12161  hash2iun  12270  2cprodeq2dv  12359  dvdsval3  12582  dvdsnegb  12599  muldvds1  12607  muldvds2  12608  dvdscmul  12609  dvdsmulc  12610  dvds2ln  12615  divalgb  12716  ndvdssub  12721  gcddiv  12820  rpexp1i  12957  phiprmpw  13028  hashgcdeq  13046  pythagtriplem1  13072  pockthg  13164  infpnlem1  13166  4sqlem3  13197  imasaddfnlemg  13693  mndpfo  13809  grplmulf1o  13937  grplactcnv  13965  mulgnn0subcl  13996  mulgsubcl  13997  mulgdir  14015  issubg2m  14050  issubgrpd2  14051  nmzsubg  14071  eqgen  14088  ghmmulg  14117  ghmf1  14134  kerf1ghm  14135  conjghm  14137  srglmhm  14403  srgrmhm  14404  ringlghm  14472  ringrghm  14473  oppr1g  14496  dvdsrcl2  14514  crngunit  14526  subsubrng  14630  subrgugrp  14656  subsubrg  14661  islmod  14735  lmodvsdir  14757  lmodvsass  14758  lsssubg  14822  lss1d  14828  lidlsubg  14931  lidlsubcl  14932  expghmap  15050  mulgghm2  15051  innei  15406  iscnp4  15461  cnpnei  15462  cnnei  15475  cnconst  15477  ismeti  15589  isxmet2d  15591  elbl2ps  15635  elbl2  15636  xblpnfps  15641  xblpnf  15642  xblm  15660  blininf  15667  blssexps  15672  blssex  15673  blsscls2  15736  metss  15737  metrest  15749  metcn  15757  divcnap  15808  cdivcncfap  15847  dvply1  16008  logdivlt  16141  lgslem4  16344  lgscllem  16348  lgsneg1  16366  lgsne0  16379  uspgr2wlkeq  16828  eupth2lem3lem7fi  16937