Theorem 3expib 1218

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 1214	. 2 |- ( ph -> ( ps -> ( ch -> th ) ) )
3	2	impd 437	1 |- ( ph -> ( ( ps /\ ch ) -> th ) )

Syntax hints:   -> wi 4   /\ wa 375   /\ w3a 991

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 190  df-an 377  df-3an 993

This theorem is referenced by:  3anidm12  1333  mob  3232  eqbrrdva  5026  fco  5766  f1oiso2  6273  frxp  6938  onfununi  7091  smoel2  7113  smoiso2  7119  3ecoptocl  7486  dffi2  7968  elfiun  7975  dif1card  8472  infxpenlem  8475  cfeq0  8717  cfsuc  8718  cfflb  8720  cfslb2n  8729  cofsmo  8730  domtriomlem  8903  axdc3lem4  8914  axdc4lem  8916  ttukey2g  8977  tskxpss  9228  grudomon  9273  elnpi  9444  dedekind  9828  nn0n0n1ge2b  10967  fzind  11067  suprzcl2  11288  icoshft  11789  fzen  11851  hashbclem  12654  seqcoll  12666  relexpsucr  13147  relexpsucl  13151  relexpfld  13167  shftuz  13187  mulgcd  14569  algcvga  14593  lcmneg  14623  ressbas  15234  resslem  15237  ressress  15242  psss  16515  tsrlemax  16521  isnmgm  16547  gsummgmpropd  16573  iscmnd  17497  ring1ne0  17876  unitmulclb  17948  isdrngd  18055  issrngd  18144  abvn0b  18581  mpfaddcl  18812  mpfmulcl  18813  pf1addcl  18996  pf1mulcl  18997  isphld  19276  fitop  19985  hausnei2  20424  ordtt1  20450  locfincmp  20596  basqtop  20781  filfi  20929  fgcl  20948  neifil  20950  filuni  20955  cnextcn  21137  prdsmet  21440  blssps  21494  blss  21495  metcnp3  21610  hlhil  22452  volsup2  22619  sincosq1sgn  23509  sincosq2sgn  23510  sincosq3sgn  23511  sincosq4sgn  23512  sinq12ge0  23519  bcmono  24261  usg2wlkonot  25667  3cyclfrgrarn1  25796  grpodivf  26030  ipf  26408  sspival  26433  shintcli  27038  spanuni  27253  adjadj  27645  unopadj2  27647  hmopadj  27648  hmopbdoptHIL  27697  resvsca  28644  resvlem  28645  submateq  28686  esumcocn  28952  bnj1379  29692  bnj571  29767  bnj594  29773  bnj580  29774  bnj600  29780  bnj1189  29868  bnj1321  29886  bnj1384  29891  ghomf1olem  30362  climuzcnv  30365  fness  31055  neificl  32128  metf1o  32130  isismty  32179  ismtybndlem  32184  ablo4pnp  32224  divrngcl  32242  keridl  32311  prnc  32346  lsmsatcv  32622  llncvrlpln2  33168  lplncvrlvol2  33226  linepsubN  33363  pmapsub  33379  dalawlem10  33491  dalawlem13  33494  dalawlem14  33495  dalaw  33497  diaf11N  34663  dibf11N  34775  ismrcd1  35586  ismrcd2  35587  mzpincl  35622  mzpadd  35626  mzpmul  35627  pellfundge  35776  imasgim  36004  stoweidlem2  37963  stoweidlem17  37978  uhgrauhgrbi  39305  is1wlkg  39775  uspgrn2crct  39922  uhgrauhgbi  40055