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

Theorem mp3an12i 1352
Description: mp3an 1348 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 1338 . 2 (𝜃𝜏)
61, 5syl 14 1 (𝜒𝜏)
Colors of variables: wff set class
Syntax hints:  wi 4  w3a 980
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 982
This theorem is referenced by:  map1  6866  exmidpw2en  6968  suplocsrlempr  7867  geo2lim  11659  fprodge0  11780  fprodge1  11782  oddp1d2  12031  bezoutlema  12136  bezoutlemb  12137  pythagtriplem1  12403  exmidunben  12583  psrelbas  14160  psraddcl  14164  ismet  14512  isxmet  14513  coseq0negpitopi  14971  cosq34lt1  14985  cos02pilt1  14986  logdivlti  15016  lgseisenlem1  15186  lgseisen  15190  m1lgs  15192
  Copyright terms: Public domain W3C validator