Theorem 3exp 830

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 775	. . 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 773

This theorem is referenced by:  3expa 831  3expb 832  3expia 833  3expib 834  3com12 835  3com23 837  3an1rs 843  3exp1 847  3expd 848  syl3an2 858  syl3an3 859  3anidm12 879  3anidm23 881  3ecase 920  sbciegf 1950  frirr 2914  wefrc 2933  tz7.7 2963  ssorduni 2983  suceloni 3052  unizlim 3103  sotri 3429  fvco2 3760  omwordri 4187  odi 4194  omass 4195  oewordri 4203  eceqopreq 4297  unxpdomlem 4815  mulcanpi 4999  divne0t 5692  divasst 5704  divmuldivt 5736  lemul1it 5793  divgt0t 5809  divge0t 5810  ltdiv2t 5835  infmsup 6015  bndndx 6020  uzind 6153  uzind2 6154  uzwo3lem1 6164  ser1add2 6275  iooval2t 6304  elfz4t 6407  sqrlem20 6622  absrpclt 6790  facavgt 6892  climsqueeze 7076  climsqueeze2 7077  caucvglem2 7094  caucvglem4 7096  isummulc1ALT 7148  neips 7668  tpnei 7675  opnneiid 7678  cnpco 7708  cnconst 7719  neibl 7817  metcn4i 7906  cmsss 7931  bcthlem1 7933  isblo3i 8392  projlem26 9127  chintcl 9210  spansncol 9407  elspansn4t 9413  osumlem4 9498  hoadddirt 9647  homco2t 9817  adjmult 9939  kbass6t 9966  spansncv2t 10130  and4as 10332  and4com 10333  infi1 10347  fiiu 10350  cnvhmpha 10412  hmphre 10417  hmeogrp 10425  efilcp 10445  fisub 10447  efilcp2 10450  iintlem1 10476  cmphmia 10570  cmphmib 10571  iri 10572  cmpassoh 10573  homgrf 10574  cmpmon 10585  icmpmon 10587

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 775

Copyright terms: Public domain