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

Theorem mp3an2i 1305
Description: mp3an 1300 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 1287 . 2 ((𝜒𝜃) → 𝜏)
61, 2, 5syl2anc 408 1 (𝜓𝜏)
Colors of variables: wff set class
Syntax hints:  wi 4  w3a 947
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 949
This theorem is referenced by:  mapen  6708  mapxpen  6710  en2eleq  7019  nnledivrp  9521  xsubge0  9632  frec2uzsucd  10142  seq3shft  10578  geolim2  11249  geoisum1c  11257  eflegeo  11335  sin01gt0  11395  cos01gt0  11396  gcdn0gt0  11593  divgcdodd  11748  sqpweven  11780  2sqpwodd  11781  ressid  11947  topnvalg  12059  restbasg  12264  restco  12270  lmfval  12288  cnfval  12290  cnpval  12294  upxp  12368  uptx  12370  txrest  12372  xblm  12513  bdmet  12598  bdmopn  12600  reopnap  12634  cnopnap  12690  dvidlemap  12756  dvcj  12769  trilpolemisumle  13158
  Copyright terms: Public domain W3C validator