Theorem 3exp 1066

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 860	. . 3 |- ((ph /\ ps /\ ch) <-> ((ph /\ ps) /\ ch))
2		3exp.1	. . 3 |- ((ph /\ ps /\ ch) -> th)
3	1, 2	sylbir 218	. 2 |- (((ph /\ ps) /\ ch) -> th)
4	3	exp31 407	1 |- (ph -> (ps -> (ch -> th)))

Syntax hints:   -> wi 3   /\ wa 240   /\ w3a 858

This theorem is referenced by:  3expa 1067  3expb 1068  3expia 1069  3expib 1070  3com12OLD 1072  3com23 1074  3an1rs 1080  3exp1 1084  3expd 1085  exp5o 1087  syl3an2 1131  syl3an3 1132  3anidm12 1154  3anidm23 1156  3ecase 1199  ee333 1279  sbciegf 2483  frirr 3634  wefrc 3652  tz7.7 3684  unizlim 3786  ssorduni 3870  ssorduniOLD 3871  suceloni 3894  sotri 4315  fvco2OLD 4738  odi 5258  omass 5259  eceqopreq 5372  ordtypelem4 5687  elomsubsd 5885  omsubindss 5888  unxpdomlem 5995  mulcanpi 6179  divmul 6896  divne0 6912  divdir 6933  ltmul1 7008  lemul1OLD 7012  lemul1a 7019  ltdiv1 7031  divgt0 7037  divge0 7038  ltmuldiv 7045  ltdiv2 7070  infmsup 7277  uzind 7417  uzind2 7418  iooval2 7534  ioojoin 7585  elfz4 7645  ser1add2i 7751  sqrlem20 7942  absrpcl 8106  facavg 8207  climsqueeze 8400  climsqueeze2 8401  isummulc1iALT 8474  neips 9003  tpnei 9010  opnneiid 9013  cnpco 9046  cnconst 9057  neibl 9154  metequiv 9158  metcn4i 9250  cmsss 9275  isga 9450  gaid 9454  vacnlem3 9669  isblo3i 9801  indexfi 10174  dif1card 10177  findcard 10178  hausnei2 10222  cnvhmpha 10240  subtopmetlem 10255  subtopmet 10256  fgfil 10290  extbas1 10291  hausfillim 10303  cncomp 10331  clmgm 10368  ismnd2 10392  grpmnd 10393  unmnd 10405  projlem26 10844  chintcli 10928  spansncol 11124  elspansn4 11129  osumlem4 11216  hoadddir 11367  homco2 11538  adjmul 11662  kbass6 11692  stadd3i 11820  spansncv2 11865  bnj1417 13530  predso 13895  tz6.26 13913  poxp 13949  poseq 13954  and4as 14266  infi1 14343  fiiu 14344  surrc2 14390  set2elt 14408  sndw 14428  surjsec 14462  injrec2 14466  surjsec2 14467  npincppr 14501  repcpwti 14503  cbcpcp 14504  cbicplem 14508  prjnpl 14510  unprj 14511  prl 14512  prl2 14514  pre2befi2 14573  preotr2 14576  prltub 14602  geme2 14617  tolat 14631  tostos 14637  latdir 14643  reacomsmgrp2 14704  clfsebs 14707  fincmpzer 14711  resgcom 14712  fprodadd 14713  fnopabco2b 14734  curgrpact 14735  grpdivone 14736  grpdivfo 14737  grpdlcan 14739  fprodneg 14741  trran2 14757  trinv 14759  zerdivemp1 14785  sum2vv 14805  mvecrtol2 14820  muldisc 14824  svli2 14826  svs2 14829  truni3 14851  hmphre 14884  hmeogrp 14892  top2ind 14897  homindlem3 14900  efilcp 14922  fisub 14924  efilcp2 14926  rcfpfillem6 14933  fbaslim2 14936  limfilnei 14943  conttnf 14944  iscnp3 14946  bwt2 14960  topgrpbs 14974  iintlem1 15010  lvsovso 15038  lvsovso2 15039  dualalg 15131  dualded 15132  dualcat2 15133  cmphmia 15147  cmphmib 15148  iri 15149  cmpassoh 15150  homgrf 15151  cmpmon 15164  icmpmon 15165  iepiclem 15172  idfisf 15189  issubcat 15193  idsubfun 15206  tarax3f 15229  tarcrpr 15237  tartord 15240  cptarc 15242  sexptrt 15243  tarsuc2 15245  tarsuc3 15246  intartar 15255  tartarmap 15265  eltintpar 15276  inttaror 15277  cartarlim 15282  fnctartar 15284  fnctartar2 15285  elicc3 15362  ioodisj 15364  finminlem 15367  ordtypelem4OLD 15378  elomsubsdOLD 15394  omsubindssOLD 15397  compsublem 15430  compsub 15431  cptclsscpt 15432  alexsublem1 15437  alexsublem4 15440  alexsub 15441  connsub 15443  reconnlem5 15450  reconn 15451  lfinpfin 15513  comppfsc 15517  ufprim 15569  filssufillem 15570  filufint 15574  ufilen 15579  filcon 15580  rnelfm 15593  filfm 15600  fcluscomp 15621  ufcomp 15622  fimax 15746  indexfiOLD 15755  inficl 15757  fisup2g 15768  iccsplit 15854  heiborlem23 15977  pcohtpy 16083  zerdivemp1x 16108  e333 16601  ordelordaxrVD 16691  luble 16806  glble 16813  joinle 16820  meetle 16827  clatlat 16893  omlfh3 16979  hlexch 17034  cvrexchlem 17059  cvrat4 17076  pointpsub 17231  paddasslem14 17294  osumcllem7 17370  osumcllem11 17374

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 164  df-an 242  df-3an 860

Copyright terms: Public domain