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

Theorem mp3an2i 1321
 Description: mp3an 1316 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 1303 . 2 ((𝜒𝜃) → 𝜏)
61, 2, 5syl2anc 409 1 (𝜓𝜏)
 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  6747  mapxpen  6749  en2eleq  7067  nnledivrp  9582  xsubge0  9693  iccen  9818  frec2uzsucd  10204  seq3shft  10641  geolim2  11312  geoisum1c  11320  ntrivcvgap  11348  eflegeo  11442  sin01gt0  11502  cos01gt0  11503  gcdn0gt0  11700  divgcdodd  11855  sqpweven  11887  2sqpwodd  11888  omctfn  11990  ressid  12057  topnvalg  12169  restbasg  12374  restco  12380  lmfval  12398  cnfval  12400  cnpval  12404  upxp  12478  uptx  12480  txrest  12482  xblm  12623  bdmet  12708  bdmopn  12710  reopnap  12744  cnopnap  12800  dvidlemap  12866  dvcj  12879  eflt  12902  logdivlti  13008  trilpolemisumle  13404
 Copyright terms: Public domain W3C validator