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

Theorem mp3an2i 1324
Description: mp3an 1319 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 1306 . 2  |-  ( ( ch  /\  th )  ->  ta )
61, 2, 5syl2anc 409 1  |-  ( ps 
->  ta )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 963
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 depends on definitions:  df-bi 116  df-3an 965
This theorem is referenced by:  mapen  6788  mapxpen  6790  en2eleq  7125  nnledivrp  9668  xsubge0  9780  iccen  9905  frec2uzsucd  10295  seq3shft  10733  geolim2  11404  geoisum1c  11412  ntrivcvgap  11440  eflegeo  11593  sin01gt0  11653  cos01gt0  11654  gcdn0gt0  11856  divgcdodd  12012  sqpweven  12044  2sqpwodd  12045  omctfn  12159  ssnnctlemct  12162  ressid  12238  topnvalg  12350  restbasg  12555  restco  12561  lmfval  12579  cnfval  12581  cnpval  12585  upxp  12659  uptx  12661  txrest  12663  xblm  12804  bdmet  12889  bdmopn  12891  reopnap  12925  cnopnap  12981  dvidlemap  13047  dvcj  13060  eflt  13083  logdivlti  13189  trilpolemisumle  13596
  Copyright terms: Public domain W3C validator