Theorem 3expib 1268

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

Syntax hints:   -> wi 4   /\ wa 384   /\ w3a 1037

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 197  df-an 386  df-3an 1039

This theorem is referenced by:  3anidm12  1383  mob  3388  eqbrrdva  5291  fco  6058  f1oiso2  6602  frxp  7287  onfununi  7438  smoel2  7460  smoiso2  7466  3ecoptocl  7839  dffi2  8329  elfiun  8336  dif1card  8833  infxpenlem  8836  cfeq0  9078  cfsuc  9079  cfflb  9081  cfslb2n  9090  cofsmo  9091  domtriomlem  9264  axdc3lem4  9275  axdc4lem  9277  ttukey2g  9338  tskxpss  9594  grudomon  9639  elnpi  9810  dedekind  10200  nn0n0n1ge2b  11359  fzind  11475  suprzcl2  11778  icoshft  12294  fzen  12358  hashbclem  13236  seqcoll  13248  relexpsucr  13769  relexpsucl  13773  relexpfld  13789  shftuz  13809  mulgcd  15265  algcvga  15292  lcmneg  15316  ressbas  15930  resslem  15933  ressress  15938  psss  17214  tsrlemax  17220  isnmgm  17246  gsummgmpropd  17275  iscmnd  18205  ring1ne0  18591  unitmulclb  18665  isdrngd  18772  issrngd  18861  rmodislmodlem  18930  rmodislmod  18931  abvn0b  19302  mpfaddcl  19534  mpfmulcl  19535  pf1addcl  19717  pf1mulcl  19718  isphld  19999  fitop  20705  hausnei2  21157  ordtt1  21183  locfincmp  21329  basqtop  21514  filfi  21663  fgcl  21682  neifil  21684  filuni  21689  cnextcn  21871  prdsmet  22175  blssps  22229  blss  22230  metcnp3  22345  hlhil  23214  volsup2  23373  sincosq1sgn  24250  sincosq2sgn  24251  sincosq3sgn  24252  sincosq4sgn  24253  sinq12ge0  24260  bcmono  25002  iswlkg  26509  umgrwwlks2on  26850  3cyclfrgrrn1  27149  grpodivf  27392  ipf  27568  shintcli  28188  spanuni  28403  adjadj  28795  unopadj2  28797  hmopadj  28798  hmopbdoptHIL  28847  resvsca  29830  resvlem  29831  submateq  29875  esumcocn  30142  bnj1379  30901  bnj571  30976  bnj594  30982  bnj580  30983  bnj600  30989  bnj1189  31077  bnj1321  31095  bnj1384  31100  climuzcnv  31565  fness  32344  neificl  33549  metf1o  33551  isismty  33600  ismtybndlem  33605  ablo4pnp  33679  divrngcl  33756  keridl  33831  prnc  33866  lsmsatcv  34297  llncvrlpln2  34843  lplncvrlvol2  34901  linepsubN  35038  pmapsub  35054  dalawlem10  35166  dalawlem13  35169  dalawlem14  35170  dalaw  35172  diaf11N  36338  dibf11N  36450  ismrcd1  37261  ismrcd2  37262  mzpincl  37297  mzpadd  37301  mzpmul  37302  pellfundge  37446  imasgim  37670  stoweidlem2  40219  stoweidlem17  40234