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

Theorem bitr4d 180
Description: Deduction form of bitr4i 176. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
bitr4d.1 (φ → (ψχ))
bitr4d.2 (φ → (θχ))
Assertion
Ref Expression
bitr4d (φ → (ψθ))

Proof of Theorem bitr4d
StepHypRef Expression
1 bitr4d.1 . 2 (φ → (ψχ))
2 bitr4d.2 . . 3 (φ → (θχ))
32bicomd 129 . 2 (φ → (χθ))
41, 3bitrd 177 1 (φ → (ψθ))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 98
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  3bitr2d  205  3bitr2rd  206  3bitr4d  209  3bitr4rd  210  bianabs  543  imordc  795  3anibar  1071  xor2dc  1278  bilukdc  1284  reuhypd  4169  opelresi  4566  iota1  4824  funbrfv2b  5161  dffn5im  5162  fneqeql  5218  f1ompt  5263  dff13  5350  fliftcnv  5378  isotr  5399  isoini  5400  caovord3  5616  releldm2  5753  tpostpos  5820  nnaordi  6017  iserd  6068  ecdmn0m  6084  qliftel  6122  qliftfun  6124  qliftf  6127  ecopovsym  6138  recmulnqg  6375  nqtri3or  6380  ltmnqg  6385  mullocprlem  6550  addextpr  6592  gt0srpr  6656  ltsosr  6672  ltasrg  6678  xrlenlt  6861  letri3  6876  subadd  6991  ltsubadd2  7203  lesubadd2  7205  suble  7210  ltsub23  7212  ltaddpos2  7223  ltsubpos  7224  subge02  7248  ltaddsublt  7335  reapneg  7361  apsym  7370  apti  7386  divmulap  7416  divmulap3  7418  rec11rap  7449  ltdiv1  7595  ltdivmul2  7605  ledivmul2  7607  ltrec  7610  nnle1eq1  7699  avgle1  7922  avgle2  7923  nn0le0eq0  7966  znnnlt1  8049  zleltp1  8055  elz2  8068  uzm1  8259  uzin  8261  difrp  8374  xrletri3  8471  xltnegi  8498  elioo5  8552  elfz5  8632  fzdifsuc  8693  elfzm11  8703  uzsplit  8704  elfzonelfzo  8836  lt2sq  8960  le2sq  8961  mulreap  9072
  Copyright terms: Public domain W3C validator