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

Theorem mp3an2i 1288
Description: mp3an 1283 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 𝜑
mp3an2i.2 (𝜓𝜒)
mp3an2i.3 (𝜓𝜃)
mp3an2i.4 ((𝜑𝜒𝜃) → 𝜏)
Assertion
Ref Expression
mp3an2i (𝜓𝜏)

Proof of Theorem mp3an2i
StepHypRef Expression
1 mp3an2i.2 . 2 (𝜓𝜒)
2 mp3an2i.3 . 2 (𝜓𝜃)
3 mp3an2i.1 . . 3 𝜑
4 mp3an2i.4 . . 3 ((𝜑𝜒𝜃) → 𝜏)
53, 4mp3an1 1270 . 2 ((𝜒𝜃) → 𝜏)
61, 2, 5syl2anc 406 1 (𝜓𝜏)
Colors of variables: wff set class
Syntax hints:  wi 4  w3a 930
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 932
This theorem is referenced by:  mapen  6669  mapxpen  6671  ctssdclemr  6911  en2eleq  6960  nnledivrp  9394  xsubge0  9505  frec2uzsucd  10015  seq3shft  10451  geolim2  11120  geoisum1c  11128  eflegeo  11206  sin01gt0  11266  cos01gt0  11267  gcdn0gt0  11461  divgcdodd  11614  sqpweven  11645  2sqpwodd  11646  ressid  11802  topnvalg  11914  restbasg  12119  restco  12125  lmfval  12143  cnfval  12145  cnpval  12148  upxp  12222  uptx  12224  txrest  12226  xblm  12345  bdmet  12430  bdmopn  12432  dvidlemap  12533  trilpolemisumle  12815
  Copyright terms: Public domain W3C validator