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 489  ancom31s 490  3impa 826  3exp 830  ax11indalem 1361  ax11inda2ALT 1362  pwssun 2816  onmindif 3050  ordsucss 3059  ordsucelsuc 3063  tfindsg 3152  tfindsg2 3153  dffo3 3804  fconstfv 3834  tfrlem9 3904  tz7.49c 3945  oaordi 4164  oaordex 4176  oaass 4179  oarec 4180  omlimcl 4193  omass 4195  oen0 4197  oeordsuc 4205  nnaordex 4233  nnawordex 4234  oaabs 4236  omsmolem 4240  sdomen2 4462  mapenlem2 4470  ssenen 4484  php3 4495  finsucdom 4506  pssnn 4513  tz9.12lem3 4633  rankr1 4646  zorn2lem6 4765  fodom 4770  ondomon 4828  alephval2 4874  axrepnd 4918  ltrpq 5057  genpcd 5081  1idpr 5105  prlem934a 5109  ltexprlem6 5119  ltexprlem7 5120  mulgt0sr 5186  recexsr 5188  ssgt0sr 5189  suppsr2 5195  suppsr3 5196  cnegext 5320  recext 5657  nnleltp1t 5901  nndivt 5906  infmrcl 6016  xrsupsslem 6023  xrinfmsslem 6024  supxrunb1 6036  supxrunb2 6037  zltp1let 6128  zneo 6147  zneoOLD 6148  uzwo4OLD 6158  qbtwnre 6216  monoord 6231  ser1add 6276  uzaddclt 6381  uzwo 6387  uzwoOLD 6388  seqzfveq 6486  expcllem 6507  expeq0t 6517  mulexpt 6525  sqr2irrlem3 6656  cjexpt 6752  absexpt 6803  seq1ublem 6848  caubnd 6863  bccl2t 6909  fsum1ps 6956  fsumadd 6960  fsummulc1 6971  fsumconst 6976  fsumcmp 6978  fsumabs 6981  clm4le 7019  clmi1 7024  climconst 7031  reccnv 7153  cvgratlem1 7185  cvgratlem5 7189  fsum0diaglem2 7192  fsum0diag2 7194  fsum0diag4 7196  ef0lem 7252  demoivre 7426  infcda 7510  topbast 7569  fctop 7592  cctop 7594  retopbas 7597  elcls 7646  elcls3 7652  islp2 7688  cnpco 7708  cnsscnp 7711  cncnplem2 7714  ssbl 7795  lmnn 7873  metelcls 7900  cmsss 7931  bcthlem21 7953  bcthlem26 7958  grpidinvlem4 7985  isgrp2i 8011  grpinvf 8014  nmosetre 8359  blocni 8396  ipasslem1 8421  ubthlem14 8473  shmods 9277  elspansn5t 9414  normcant 9416  h1datom 9421  osumlem4 9498  osumlem6 9500  nmopsetretALT 9707  nmfnsetret 9721  lnopcon 9878  lnfncon 9905  bra11 9954  cnvbravalt 9956  pjnmop 9986  pjss2co 10003  pj3cor1 10047  mdexch 10170  superpos 10189  atcvat4 10232  mdsymlem3 10240  mdsymlem4 10241  sumdmdi 10249  cdj3lem2b 10269  cnrsfin 10396  cnrscoa 10397  cnvhmphb 10413  qusp 10430  efilcp 10445  trnij 10481  ismonc 10584

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