ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  expr Unicode version

Theorem expr 370
Description: Export a wff from a right conjunct. (Contributed by Jeff Hankins, 30-Aug-2009.)
Hypothesis
Ref Expression
expr.1  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  ->  th )
Assertion
Ref Expression
expr  |-  ( (
ph  /\  ps )  ->  ( ch  ->  th )
)

Proof of Theorem expr
StepHypRef Expression
1 expr.1 . . 3  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  ->  th )
21exp32 360 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
32imp 123 1  |-  ( (
ph  /\  ps )  ->  ( ch  ->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem is referenced by:  animpimp2impd  531  reximddv  2510  rexlimdvaa  2525  issod  4209  ordsuc  4446  fcof1  5650  riota5f  5720  ovmpodf  5868  tfrlemi1  6195  eqsuptid  6850  eqinftid  6874  ordiso2  6886  addnq0mo  7219  mulnq0mo  7220  genprndl  7293  genprndu  7294  addlocpr  7308  ltexprlemm  7372  ltexprlemopl  7373  ltexprlemopu  7375  ltexprlemfl  7381  ltexprlemfu  7383  aptiprleml  7411  caucvgprprlemexbt  7478  addsrmo  7515  mulsrmo  7516  prodge0  8569  un0addcl  8961  un0mulcl  8962  seq3fveq2  10182  seq3shft2  10186  monoord  10189  seq3split  10192  seq3id2  10222  expnegzap  10267  expcanlem  10402  bcval5  10449  seq3coll  10525  caucvgrelemcau  10692  cau3lem  10826  reccn2ap  11022  summodclem2  11091  zsumdc  11093  fsumf1o  11099  fisumss  11101  fsumcl2lem  11107  fsumadd  11115  fisum0diag2  11156  fsummulc2  11157  mertenslem2  11245  dvds0lem  11399  dvdsnegb  11406  dvdssub2  11431  isprm6  11721  hashgcdeq  11799  topssnei  12226  innei  12227  cnptopco  12286  cncnpi  12292  cncnp  12294  cnconst2  12297  cnpdis  12306  lmtopcnp  12314  tx2cn  12334  txdis  12341  blssps  12491  blss  12492  neibl  12555  metss  12558  metequiv2  12560  metrest  12570  metcnp3  12575
  Copyright terms: Public domain W3C validator