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

Theorem mp3an12i 1341
Description: mp3an 1337 with antecedents in standard conjunction form and with one hypothesis an implication. (Contributed by Alan Sare, 28-Aug-2016.)
Hypotheses
Ref Expression
mp3an12i.1  |-  ph
mp3an12i.2  |-  ps
mp3an12i.3  |-  ( ch 
->  th )
mp3an12i.4  |-  ( (
ph  /\  ps  /\  th )  ->  ta )
Assertion
Ref Expression
mp3an12i  |-  ( ch 
->  ta )

Proof of Theorem mp3an12i
StepHypRef Expression
1 mp3an12i.3 . 2  |-  ( ch 
->  th )
2 mp3an12i.1 . . 3  |-  ph
3 mp3an12i.2 . . 3  |-  ps
4 mp3an12i.4 . . 3  |-  ( (
ph  /\  ps  /\  th )  ->  ta )
52, 3, 4mp3an12 1327 . 2  |-  ( th 
->  ta )
61, 5syl 14 1  |-  ( ch 
->  ta )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 978
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108
This theorem depends on definitions:  df-bi 117  df-3an 980
This theorem is referenced by:  map1  6806  suplocsrlempr  7794  geo2lim  11505  fprodge0  11626  fprodge1  11628  oddp1d2  11875  bezoutlema  11980  bezoutlemb  11981  pythagtriplem1  12245  exmidunben  12407  ismet  13504  isxmet  13505  coseq0negpitopi  13917  cosq34lt1  13931  cos02pilt1  13932  logdivlti  13962
  Copyright terms: Public domain W3C validator