Theorem 3exp 838

Description: Exportation inference.

Hypothesis

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

Assertion

Ref	Expression
3exp	|- (ph -> (ps -> (ch -> th)))

Proof of Theorem 3exp

Step	Hyp	Ref	Expression
1		df-3an 783	. . 3 |- ((ph /\ ps /\ ch) <-> ((ph /\ ps) /\ ch))
2		3exp.1	. . 3 |- ((ph /\ ps /\ ch) -> th)
3	1, 2	sylbir 199	. 2 |- (((ph /\ ps) /\ ch) -> th)
4	3	exp31 376	1 |- (ph -> (ps -> (ch -> th)))

Syntax hints:   -> wi 3   /\ wa 221   /\ w3a 781

This theorem is referenced by:  3expa 839  3expb 840  3expia 841  3expib 842  3com12 843  3com23 845  3an1rs 851  3exp1 855  3expd 856  syl3an2 866  syl3an3 867  3anidm12 888  3anidm23 890  3ecase 930  sbciegf 2008  frirr 2954  wefrc 2970  tz7.7 3001  unizlim 3086  ssorduni 3147  suceloni 3170  sotri 3535  fvco2 3886  omwordri 4339  odi 4346  omass 4347  oewordri 4355  eceqopreq 4454  unxpdomlem 4993  mulcanpi 5181  divmul 5859  divne0 5875  divdir 5896  ltmul1 5970  lemul1OLD 5974  lemul1a 5981  ltdiv1 5993  divgt0 5999  divge0 6000  ltmuldiv 6007  ltdiv2 6032  infmsup 6236  bndndx 6241  uzind 6376  uzind2 6377  uzwo3lem1 6388  iooval2 6493  ioojoin 6543  elfz4 6603  ser1add2i 6703  sqrlem20 6893  absrpcl 7057  facavg 7158  climsqueeze 7343  climsqueeze2 7344  caucvglem2 7361  caucvglem4 7363  isummulc1iALT 7417  neips 7937  tpnei 7944  opnneiid 7947  cnpco 7979  cnconst 7990  neibl 8087  metequiv 8091  metcn4i 8183  cmsss 8208  bcthlem1 8210  vacnlem3 8584  isblo3i 8716  projlem26 9487  chintcli 9571  spansncol 9767  elspansn4 9772  osumlem4 9859  hoadddir 10010  homco2 10180  adjmul 10304  kbass6 10334  stadd3i 10456  spansncv2 10501  and4as 10716  and4com 10717  infi1 10735  fiiu 10738  set2elt 10827  tostos 10883  ismnd2 10928  grpmnd 10933  unmnd 10951  truni3 11001  cnvhmpha 11031  hmphre 11036  hmeogrp 11044  top2ind 11050  homindlem3 11053  efilcp 11083  fisub 11085  efilcp2 11087  rcfpfillem6 11094  bwt2 11123  iintlem1 11155  cmphmia 11253  cmphmib 11254  iri 11255  cmpassoh 11256  homgrf 11257  cmpmon 11270  icmpmon 11271  iepiclem 11278  idfisf 11295  issubcat 11299  idsubfun 11312  exp5o 11385  elicc3 11410  ioodisj 11413  finminlem 11418  ordtypelem4 11430  elomsubsd 11446  omsubindss 11449  hausnei2 11471  compsublem 11487  compsub 11488  cptclsscpt 11489  cncomp 11494  alexsublem1 11496  alexsublem4 11499  alexsub 11500  connsub 11502  subtopmetlem 11505  subtopmet 11506  reconnlem5 11511  reconn 11512  lfinpfin 11574  comppfsc 11578  fgfil 11638  extbas1 11641  ufprim 11654  filssufillem 11655  filufint 11659  ufilen 11664  filcon 11665  hausfillim 11685  rnelfm 11699  filfm 11706  fcluscomp 11733  ufcomp 11734  isga 11772  gaid 11776  dif1card 11835  fimax 11837  indexf 11847  inficl 11849  iccsplit 11919  heiborlem23 12033  heiborlem32 12042  rrntotbndlem2 12077

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

This theorem depends on definitions:  df-bi 145  df-an 223  df-3an 783

Copyright terms: Public domain