Theorem 3exp 831

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

Syntax hints:   -> wi 3   /\ wa 223   /\ w3a 774

This theorem is referenced by:  3expa 832  3expb 833  3expia 834  3expib 835  3com12 836  3com23 838  3an1rs 844  3exp1 848  3expd 849  syl3an2 859  syl3an3 860  3anidm12 881  3anidm23 883  3ecase 922  sbciegf 1957  frirr 2920  wefrc 2939  tz7.7 2969  ssorduni 2989  suceloni 3058  unizlim 3109  sotri 3439  fvco2 3770  omwordri 4196  odi 4203  omass 4204  oewordri 4212  eceqopreq 4306  unxpdomlem 4826  mulcanpi 5010  ltneOLD 5567  divne0t 5702  divasst 5714  divmuldivt 5746  lemul1it 5803  divgt0t 5819  divge0t 5820  ltdiv2t 5845  infmsup 6025  bndndx 6030  uzind 6163  uzind2 6164  uzwo3lem1 6174  ser1add2 6288  iooval2t 6317  elfz4t 6420  sqrlem20 6637  absrpclt 6805  facavgt 6907  climsqueeze 7093  climsqueeze2 7094  caucvglem2 7111  caucvglem4 7113  isummulc1ALT 7165  znnenlemOLD 7461  neips 7687  tpnei 7694  opnneiid 7697  cnpco 7729  cnconst 7740  neibl 7839  metcn4i 7934  cmsss 7959  bcthlem1 7961  isblo3i 8420  projlem26 9166  chintcl 9250  spansncol 9447  elspansn4t 9453  osumlem4 9538  hoadddirt 9687  homco2t 9858  adjmult 9981  kbass6t 10010  stadd3 10131  spansncv2t 10176  and4as 10390  and4com 10391  infi1 10405  fiiu 10408  cnvhmpha 10471  hmphre 10476  hmeogrp 10484  efilcp 10504  fisub 10506  efilcp2 10509  rcfpfillem6 10516  iintlem1 10548  cmphmia 10642  cmphmib 10643  iri 10644  cmpassoh 10645  homgrf 10646  cmpmon 10657  icmpmon 10659  idfisf 10670

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 147  df-an 225  df-3an 776

Copyright terms: Public domain