Theorem exp31 378

Description: An exportation inference.

Hypothesis

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

Assertion

Ref	Expression
exp31	|- (ph -> (ps -> (ch -> th)))

Proof of Theorem exp31

Step	Hyp	Ref	Expression
1		exp31.1	. . 3 |- (((ph /\ ps) /\ ch) -> th)
2	1	ex 373	. 2 |- ((ph /\ ps) -> (ch -> th))
3	2	ex 373	1 |- (ph -> (ps -> (ch -> th)))

Syntax hints:   -> wi 3   /\ wa 223

This theorem is referenced by:  exp41 384  exp42 385  adantlll 398  adantllr 399  adantlrl 400  adantlrr 401  anasss 442  ancom1s 492  ancom31s 493  3impa 830  3exp 834  ax11indalem 1370  ax11inda2ALT 1371  pwssun 2833  onmindif 3066  ordsucss 3075  ordsucelsuc 3079  tfindsg 3168  tfindsg2 3169  dffo3 3825  fconstfv 3855  tfrlem9 3925  tz7.49c 3966  oaordi 4186  oaordex 4198  oaass 4201  oarec 4202  omlimcl 4215  omass 4217  oen0 4219  oeordsuc 4227  nnaordex 4255  nnawordex 4256  oaabs 4258  omsmolem 4262  sdomen2 4488  mapenlem2 4496  ssenen 4510  php3 4521  php3OLD 4522  finsucdom 4532  finsucdomOLD 4533  pssnn 4544  tz9.12lem3 4671  rankr1 4684  zorn2lem6 4803  fodom 4808  ondomon 4867  alephval2 4913  axrepnd 4958  ltrpq 5097  genpcd 5121  1idpr 5145  prlem934a 5149  ltexprlem6 5159  ltexprlem7 5160  mulgt0sr 5226  recexsr 5228  ssgt0sr 5229  suppsr2 5235  suppsr3 5236  cnegext 5360  recext 5696  nnleltp1t 5956  nndivt 5961  infmrcl 6071  xrsupsslem 6078  xrinfmsslem 6079  supxrunb1 6091  supxrunb2 6092  zltp1let 6183  zneo 6202  uzwo4OLD 6212  qbtwnre 6279  monoord 6295  ser1add 6340  uzaddclt 6450  uzwo 6456  uzwoOLD 6457  seqzfveq 6555  expcllem 6576  expeq0t 6586  mulexpt 6595  sqr2irrlem3 6727  cjexpt 6817  absexpt 6868  seq1ublem 6911  caubnd 6926  bccl2t 6971  fsum1ps 7018  fsumadd 7022  fsummulc1 7033  fsumconst 7038  fsumcmp 7040  fsumabs 7043  clm4le 7081  clmi1 7086  climconst 7094  reccnv 7218  cvgratlem1 7250  cvgratlem5 7254  fsum0diaglem2 7257  fsum0diag2 7259  fsum0diag4 7261  ef0lem 7310  demoivre 7485  infcda 7568  topbast 7626  fctopOLD 7647  cctop 7649  retopbas 7652  elcls 7701  elcls3 7708  islp2 7744  cnpco 7766  cnsscnp 7769  cncnplem2 7772  ssbl 7852  lmnn 7932  metelcls 7962  cmsss 7994  bcthlem21 8016  bcthlem26 8021  grpidinvlem4 8048  isgrp2i 8072  grpinvf 8075  nmosetre 8423  blocni 8461  ipasslem1 8486  ubthlem14 8538  shmods 9357  elspansn5t 9492  normcant 9494  h1datom 9499  osumlem4 9576  osumlem6 9578  nmopsetretALT 9785  nmfnsetret 9799  lnopcon 9958  lnfncon 9985  bra11 10036  cnvbravalt 10038  pjnmop 10070  pjss2co 10087  pj3cor1 10132  mdexch 10257  superpos 10276  atcvat4 10319  mdsymlem3 10327  mdsymlem4 10328  sumdmdi 10337  cdj3lem2b 10359  cnrsfin 10495  cnrscoa 10496  cnvhmphb 10512  qusp 10541  efilcp 10556  trnij 10608  ismonc 10713

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

Copyright terms: Public domain