Theorem exp31 376

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 382  exp42 383  adantlll 396  adantllr 397  adantlrl 398  adantlrr 399  anasss 440  ancom1s 490  ancom31s 491  3impa 827  3exp 831  ax11indalem 1368  ax11inda2ALT 1369  pwssun 2824  onmindif 3057  ordsucss 3066  ordsucelsuc 3070  tfindsg 3159  tfindsg2 3160  dffo3 3816  fconstfv 3846  tfrlem9 3916  tz7.49c 3957  oaordi 4177  oaordex 4189  oaass 4192  oarec 4193  omlimcl 4206  omass 4208  oen0 4210  oeordsuc 4218  nnaordex 4246  nnawordex 4247  oaabs 4249  omsmolem 4253  sdomen2 4475  mapenlem2 4483  ssenen 4497  php3 4508  finsucdom 4519  pssnn 4526  tz9.12lem3 4648  rankr1 4661  zorn2lem6 4780  fodom 4785  ondomon 4843  alephval2 4889  axrepnd 4933  ltrpq 5072  genpcd 5096  1idpr 5120  prlem934a 5124  ltexprlem6 5134  ltexprlem7 5135  mulgt0sr 5201  recexsr 5203  ssgt0sr 5204  suppsr2 5210  suppsr3 5211  cnegext 5335  recext 5671  nnleltp1t 5915  nndivt 5920  infmrcl 6030  xrsupsslem 6037  xrinfmsslem 6038  supxrunb1 6050  supxrunb2 6051  zltp1let 6142  zneo 6161  zneoOLD 6162  uzwo4OLD 6172  qbtwnre 6233  monoord 6249  ser1add 6294  uzaddclt 6399  uzwo 6405  uzwoOLD 6406  seqzfveq 6504  expcllem 6525  expeq0t 6535  mulexpt 6544  sqr2irrlem3 6677  cjexpt 6778  absexpt 6830  seq1ublem 6877  caubnd 6892  bccl2t 6939  fsum1ps 6986  fsumadd 6990  fsummulc1 7001  fsumconst 7006  fsumcmp 7008  fsumabs 7011  clm4le 7049  clmi1 7054  climconst 7062  reccnv 7189  cvgratlem1 7221  cvgratlem5 7225  fsum0diaglem2 7228  fsum0diag2 7230  fsum0diag4 7232  ef0lem 7288  demoivre 7462  infcda 7546  topbast 7606  fctop 7629  cctop 7631  retopbas 7634  elcls 7683  elcls3 7690  islp2 7726  cnpco 7748  cnsscnp 7751  cncnplem2 7754  ssbl 7838  lmnn 7918  metelcls 7948  cmsss 7980  bcthlem21 8002  bcthlem26 8007  grpidinvlem4 8034  isgrp2i 8059  grpinvf 8062  nmosetre 8412  blocni 8449  ipasslem1 8474  ubthlem14 8526  shmods 9350  elspansn5t 9487  normcant 9489  h1datom 9494  osumlem4 9571  osumlem6 9573  nmopsetretALT 9781  nmfnsetret 9795  lnopcon 9954  lnfncon 9981  bra11 10032  cnvbravalt 10034  pjnmop 10066  pjss2co 10083  pj3cor1 10128  mdexch 10253  superpos 10272  atcvat4 10315  mdsymlem3 10323  mdsymlem4 10324  sumdmdi 10333  cdj3lem2b 10355  cnrsfin 10490  cnrscoa 10491  cnvhmphb 10507  qusp 10524  efilcp 10539  trnij 10588  ismonc 10691

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