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

Theorem mp3an12i 1323
Description: mp3an 1319 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 1309 . 2 (𝜃𝜏)
61, 5syl 14 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:  map1  6757  suplocsrlempr  7727  geo2lim  11413  fprodge0  11534  fprodge1  11536  oddp1d2  11780  bezoutlema  11882  bezoutlemb  11883  exmidunben  12155  ismet  12744  isxmet  12745  coseq0negpitopi  13157  cosq34lt1  13171  cos02pilt1  13172  logdivlti  13202
  Copyright terms: Public domain W3C validator