Theorem 3expib 1200

Description: Exportation from triple conjunction. (Contributed by NM, 19-May-2007.)

Hypothesis

Ref	Expression
3exp.1	|- ( ( ph /\ ps /\ ch ) -> th )

Assertion

Ref	Expression
3expib	|- ( ph -> ( ( ps /\ ch ) -> th ) )

Proof of Theorem 3expib

Step	Hyp	Ref	Expression
1		3exp.1	. . 3 |- ( ( ph /\ ps /\ ch ) -> th )
2	1	3exp 1196	. 2 |- ( ph -> ( ps -> ( ch -> th ) ) )
3	2	impd 429	1 |- ( ph -> ( ( ps /\ ch ) -> th ) )

Syntax hints:   -> wi 4   /\ wa 367   /\ w3a 974

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 185  df-an 369  df-3an 976

This theorem is referenced by:  3anidm12  1287  mob  3231  eqbrrdva  4993  fco  5724  f1oiso2  6231  frxp  6894  onfununi  7045  smoel2  7067  smoiso2  7073  3ecoptocl  7440  dffi2  7917  elfiun  7924  dif1card  8420  infxpenlem  8423  cfeq0  8668  cfsuc  8669  cfflb  8671  cfslb2n  8680  cofsmo  8681  domtriomlem  8854  axdc3lem4  8865  axdc4lem  8867  ttukey2g  8928  tskxpss  9180  grudomon  9225  elnpi  9396  dedekind  9778  nn0n0n1ge2b  10901  fzind  11001  suprzcl2  11217  icoshft  11696  fzen  11757  hashbclem  12550  seqcoll  12561  relexpsucr  13011  relexpsucl  13015  relexpfld  13031  shftuz  13051  mulgcd  14393  algcvga  14417  ressbas  14898  resslem  14901  ressress  14906  psss  16168  tsrlemax  16174  isnmgm  16200  gsummgmpropd  16226  iscmnd  17134  ring1ne0  17559  unitmulclb  17634  isdrngd  17741  issrngd  17830  abvn0b  18271  mpfaddcl  18523  mpfmulcl  18524  pf1addcl  18709  pf1mulcl  18710  isphld  18987  fitop  19701  hausnei2  20147  ordtt1  20173  locfincmp  20319  basqtop  20504  filfi  20652  fgcl  20671  neifil  20673  filuni  20678  cnextcn  20859  prdsmet  21165  blssps  21219  blss  21220  metcnp3  21335  hlhil  22150  volsup2  22306  sincosq1sgn  23183  sincosq2sgn  23184  sincosq3sgn  23185  sincosq4sgn  23186  sinq12ge0  23193  bcmono  23933  usg2wlkonot  25300  3cyclfrgrarn1  25429  grpodivf  25662  ipf  26040  sspival  26065  shintcli  26661  spanuni  26876  adjadj  27268  unopadj2  27270  hmopadj  27271  hmopbdoptHIL  27320  resvsca  28273  resvlem  28274  esumcocn  28527  bnj1379  29216  bnj571  29291  bnj594  29297  bnj580  29298  bnj600  29304  bnj1189  29392  bnj1321  29410  bnj1384  29415  ghomf1olem  29886  climuzcnv  29889  fness  30577  neificl  31528  metf1o  31530  isismty  31579  ismtybndlem  31584  ablo4pnp  31624  divrngcl  31642  keridl  31711  prnc  31746  lsmsatcv  32028  llncvrlpln2  32574  lplncvrlvol2  32632  linepsubN  32769  pmapsub  32785  dalawlem10  32897  dalawlem13  32900  dalawlem14  32901  dalaw  32903  diaf11N  34069  dibf11N  34181  ismrcd1  34992  ismrcd2  34993  mzpincl  35028  mzpadd  35032  mzpmul  35033  pellfundge  35179  imasgim  35412  lcmneg  36057  stoweidlem2  37152  stoweidlem17  37167  uhgrauhgbi  38003