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

Theorem mp3an12i 1341
Description: mp3an 1337 with antecedents in standard conjunction form and with one hypothesis an implication. (Contributed by Alan Sare, 28-Aug-2016.)
Hypotheses
Ref Expression
mp3an12i.1 𝜑
mp3an12i.2 𝜓
mp3an12i.3 (𝜒𝜃)
mp3an12i.4 ((𝜑𝜓𝜃) → 𝜏)
Assertion
Ref Expression
mp3an12i (𝜒𝜏)

Proof of Theorem mp3an12i
StepHypRef Expression
1 mp3an12i.3 . 2 (𝜒𝜃)
2 mp3an12i.1 . . 3 𝜑
3 mp3an12i.2 . . 3 𝜓
4 mp3an12i.4 . . 3 ((𝜑𝜓𝜃) → 𝜏)
52, 3, 4mp3an12 1327 . 2 (𝜃𝜏)
61, 5syl 14 1 (𝜒𝜏)
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:  map1  6811  suplocsrlempr  7805  geo2lim  11519  fprodge0  11640  fprodge1  11642  oddp1d2  11889  bezoutlema  11994  bezoutlemb  11995  pythagtriplem1  12259  exmidunben  12421  ismet  13775  isxmet  13776  coseq0negpitopi  14188  cosq34lt1  14202  cos02pilt1  14203  logdivlti  14233
  Copyright terms: Public domain W3C validator