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  6683  oawordriexmid  6747  mapxpen  7152  findcard  7196  findcard2  7197  findcard2s  7198  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  9745  fzind  9772  fnn0ind  9773  uzss  9959  qmulcl  10053  qreccl  10058  xrlttr  10214  xaddass  10288  icc0r  10345  iooshf  10371  elfz5  10437  elfz0fzfz0  10550  fzind2  10675  ioo0  10711  ico0  10713  ioc0  10714  expnegap0  11005  expineg2  11006  mulexpzap  11037  expsubap  11045  expnbnd  11122  facndiv  11199  bccmpl  11214  bcval5  11223  bcpasc  11226  ccatrn  11399  swrdspsleq  11461  swrdccat2  11465  ccatpfx  11495  pfxccat1  11496  swrdswrd  11499  cats1un  11515  crim  11645  climshftlemg  12093  2sumeq2dv  12162  hash2iun  12271  2cprodeq2dv  12360  dvdsval3  12583  dvdsnegb  12600  muldvds1  12608  muldvds2  12609  dvdscmul  12610  dvdsmulc  12611  dvds2ln  12616  divalgb  12717  ndvdssub  12722  gcddiv  12821  rpexp1i  12958  phiprmpw  13029  hashgcdeq  13047  pythagtriplem1  13073  pockthg  13165  infpnlem1  13167  4sqlem3  13198  imasaddfnlemg  13694  mndpfo  13810  grplmulf1o  13938  grplactcnv  13966  mulgnn0subcl  13997  mulgsubcl  13998  mulgdir  14016  issubg2m  14051  issubgrpd2  14052  nmzsubg  14072  eqgen  14089  ghmmulg  14118  ghmf1  14135  kerf1ghm  14136  conjghm  14138  srglmhm  14404  srgrmhm  14405  ringlghm  14473  ringrghm  14474  oppr1g  14497  dvdsrcl2  14515  crngunit  14527  subsubrng  14631  subrgugrp  14657  subsubrg  14662  islmod  14736  lmodvsdir  14758  lmodvsass  14759  lsssubg  14823  lss1d  14829  lidlsubg  14932  lidlsubcl  14933  expghmap  15051  mulgghm2  15052  innei  15389  iscnp4  15444  cnpnei  15445  cnnei  15458  cnconst  15460  ismeti  15572  isxmet2d  15574  elbl2ps  15618  elbl2  15619  xblpnfps  15624  xblpnf  15625  xblm  15643  blininf  15650  blssexps  15655  blssex  15656  blsscls2  15719  metss  15720  metrest  15732  metcn  15740  divcnap  15791  cdivcncfap  15830  dvply1  15991  logdivlt  16124  lgslem4  16327  lgscllem  16331  lgsneg1  16349  lgsne0  16362  uspgr2wlkeq  16811  eupth2lem3lem7fi  16920