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 371	. 2 |- ((ph /\ ps) -> (ch -> th))
3	2	ex 371	1 |- (ph -> (ps -> (ch -> th)))

Syntax hints:   -> wi 3   /\ wa 221

This theorem is referenced by:  exp41 382  exp42 383  adantlll 396  adantllr 397  adantlrl 398  adantlrr 399  anasss 442  ancom1s 492  ancom31s 493  3impa 831  3exp 835  ax11indalem 1401  ax11inda2ALT 1402  pwssun 2881  onmindif 3115  ordsucss 3124  ordsucelsuc 3128  tfindsg 3187  tfindsg2 3188  dffo3 3895  fconstfv 3925  tfrlem9 3995  tz7.49c 4036  oaordi 4264  oaordex 4276  oaass 4279  oarec 4280  omlimcl 4293  omass 4295  oen0 4297  oeordsuc 4305  nnaordex 4333  nnawordex 4334  oaabs 4336  omsmolem 4340  sdomen2 4569  mapenlem2 4579  ssenen 4593  php3 4604  finsucdom 4615  pssnn 4623  tz9.12lem3 4747  rankr1 4760  zorn2lem6 4879  fodom 4884  ondomon 4945  alephval2 4991  axrepnd 5035  ltrpq 5174  genpcd 5198  1idpr 5222  prlem934a 5226  ltexprlem6 5236  ltexprlem7 5237  mulgt0sr 5303  recexsr 5305  ssgt0sr 5306  suppsr2 5312  suppsr3 5313  cnegex 5437  recex 5773  nnleltp1 6042  nndiv 6047  infmrcl 6179  xrsupsslem 6186  xrinfmsslem 6187  supxrunb1 6199  supxrunb2 6200  zltp1le 6291  zdiv 6298  zneo 6313  uzwo4OLD 6323  qbtwnre 6359  monoord 6415  uzaddcl 6509  uzwo 6515  uzwoOLD 6516  ser1addi 6632  seqzfveq 6677  expcllem 6698  expeq0 6708  mulexp 6717  sqr2irrlem3 6849  cjexp 6940  absexp 6991  seq1ublem 7034  caubndi 7049  bccl2 7094  fsum1ps 7141  fsumadd 7145  fsummulc1 7156  fsumconst 7161  fsumcmp 7163  fsumabs 7166  clm4lei 7204  clmi1i 7209  climconsti 7217  reccnv 7341  cvgratlem1 7373  cvgratlem5 7377  fsum0diaglem2 7380  fsum0diag2 7382  fsum0diag4 7384  ef0lem 7433  demoivre 7609  infcda 7692  topbas 7751  cctop 7772  retopbas 7775  elcls 7824  elcls3 7831  islp2 7867  cnpco 7889  cnsscnp 7892  cncnplem2 7895  ssbl 7975  lmnn 8055  metelcls 8085  cmsss 8117  bcthlem21 8139  bcthlem26 8144  grpidinvlem4 8171  isgrp2i 8195  grpinvf 8198  nmosetre 8546  blocni 8584  ipasslem1 8609  ubthlem14 8661  shmodsi 9482  elspansn5 9617  normcan 9619  h1datomi 9624  osumlem4 9701  osumlem6 9703  nmopsetretALT 9908  nmfnsetre 9922  lnopconi 10080  lnfnconi 10107  bra11 10158  cnvbraval 10160  pjnmopi 10192  pjss2coi 10209  pj3cor1i 10255  mdexchi 10380  superpos 10399  atcvat4i 10442  mdsymlem3 10450  mdsymlem4 10451  sumdmdii 10460  cdj3lem2b 10482  cnrsfin 10645  cnrscoa 10646  cnvhmphb 10662  qusp 10694  efilcp 10709  usinuniop 10753  trnij 10773  ismonc 10877  isepic 10887

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 145  df-an 223

Copyright terms: Public domain