MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  exp4b Unicode version

Theorem exp4b 590
Description: An exportation inference. (Contributed by NM, 26-Apr-1994.) (Proof shortened by Wolf Lammen, 23-Nov-2012.)
Hypothesis
Ref Expression
exp4b.1  |-  ( (
ph  /\  ps )  ->  ( ( ch  /\  th )  ->  ta )
)
Assertion
Ref Expression
exp4b  |-  ( ph  ->  ( ps  ->  ( ch  ->  ( th  ->  ta ) ) ) )

Proof of Theorem exp4b
StepHypRef Expression
1 exp4b.1 . . 3  |-  ( (
ph  /\  ps )  ->  ( ( ch  /\  th )  ->  ta )
)
21ex 423 . 2  |-  ( ph  ->  ( ps  ->  (
( ch  /\  th )  ->  ta ) ) )
32exp4a 589 1  |-  ( ph  ->  ( ps  ->  ( ch  ->  ( th  ->  ta ) ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358
This theorem is referenced by:  exp43  595  reuss2  3461  somo  4364  tz7.7  4434  f1oweALT  5867  onfununi  6374  odi  6593  omeu  6599  nndi  6637  inf3lem2  7346  axdc3lem2  8093  genpnmax  8647  mulclprlem  8659  distrlem5pr  8667  reclem4pr  8690  mulcmpblnr  8712  lemul12a  9630  sup2  9726  nnmulcl  9785  zbtwnre  10330  le2sq2  11195  expnbnd  11246  dvdslegcd  12711  unbenlem  12971  infpnlem1  12973  lmodvsdi  15666  lspsolvlem  15911  lbsextlem2  15928  1stccnp  17204  itg2le  19110  spansneleq  22165  elspansn4  22168  cvmdi  22920  atcvat3i  22992  mdsymlem3  23001  dfon2lem8  24217  soseq  24325  nodenselem5  24410  areacirclem2  25028  areacirclem3  25029  areacirclem4  25030  areacirclem5  25032  areacirc  25034  rspc2edv  25066  icmpmon  25919  fzmul  26546  cvlexch1  30140  hlrelat2  30214  cvrat3  30253  snatpsubN  30561  pmaple  30572
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360
  Copyright terms: Public domain W3C validator