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

Theorem mp3an2i 1342
Description: mp3an 1337 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 1324 . 2  |-  ( ( ch  /\  th )  ->  ta )
61, 2, 5syl2anc 411 1  |-  ( ps 
->  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:  mapen  6845  mapxpen  6847  en2eleq  7193  nnledivrp  9765  xsubge0  9880  iccen  10005  frec2uzsucd  10400  seq3shft  10846  geolim2  11519  geoisum1c  11527  ntrivcvgap  11555  eflegeo  11708  sin01gt0  11768  cos01gt0  11769  gcdn0gt0  11978  uzwodc  12037  divgcdodd  12142  sqpweven  12174  2sqpwodd  12175  pythagtriplem4  12267  pythagtriplem11  12273  pythagtriplem12  12274  pythagtriplem13  12275  pythagtriplem14  12276  pcfac  12347  omctfn  12443  ssnnctlemct  12446  topnvalg  12699  imasmulr  12729  imasaddfnlemg  12734  ismhm  12852  scaffng  13397  zringinvg  13464  restbasg  13638  restco  13644  lmfval  13662  cnfval  13664  cnpval  13668  upxp  13742  uptx  13744  txrest  13746  xblm  13887  bdmet  13972  bdmopn  13974  reopnap  14008  cnopnap  14064  dvidlemap  14130  dvcj  14143  eflt  14166  logdivlti  14272  trilpolemisumle  14756
  Copyright terms: Public domain W3C validator