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

Theorem mp3an2i 1279
Description: mp3an 1274 with antecedents in standard conjunction form and with two hypotheses which are implications. (Contributed by Alan Sare, 28-Aug-2016.)
Hypotheses
Ref Expression
mp3an2i.1  |-  ph
mp3an2i.2  |-  ( ps 
->  ch )
mp3an2i.3  |-  ( ps 
->  th )
mp3an2i.4  |-  ( (
ph  /\  ch  /\  th )  ->  ta )
Assertion
Ref Expression
mp3an2i  |-  ( ps 
->  ta )

Proof of Theorem mp3an2i
StepHypRef Expression
1 mp3an2i.2 . 2  |-  ( ps 
->  ch )
2 mp3an2i.3 . 2  |-  ( ps 
->  th )
3 mp3an2i.1 . . 3  |-  ph
4 mp3an2i.4 . . 3  |-  ( (
ph  /\  ch  /\  th )  ->  ta )
53, 4mp3an1 1261 . 2  |-  ( ( ch  /\  th )  ->  ta )
61, 2, 5syl2anc 404 1  |-  ( ps 
->  ta )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 925
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116  df-3an 927
This theorem is referenced by:  mapen  6616  mapxpen  6618  en2eleq  6882  nnledivrp  9298  frec2uzsucd  9869  seq3shft  10333  geolim2  10967  geoisum1c  10975  eflegeo  11053  sin01gt0  11113  cos01gt0  11114  gcdn0gt0  11308  divgcdodd  11461  sqpweven  11492  2sqpwodd  11493  ressid  11616  topnvalg  11725
  Copyright terms: Public domain W3C validator