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  6551  addextpr  6593  gt0srpr  6676  ltsosr  6692  ltasrg  6698  xrlenlt  6881  letri3  6896  subadd  7011  ltsubadd2  7223  lesubadd2  7225  suble  7230  ltsub23  7232  ltaddpos2  7243  ltsubpos  7244  subge02  7268  ltaddsublt  7355  reapneg  7381  apsym  7390  apti  7406  divmulap  7436  divmulap3  7438  rec11rap  7469  ltdiv1  7615  ltdivmul2  7625  ledivmul2  7627  ltrec  7630  nnle1eq1  7719  avgle1  7942  avgle2  7943  nn0le0eq0  7986  znnnlt1  8069  zleltp1  8075  elz2  8088  uzm1  8279  uzin  8281  difrp  8394  xrletri3  8491  xltnegi  8518  elioo5  8572  elfz5  8652  fzdifsuc  8713  elfzm11  8723  uzsplit  8724  elfzonelfzo  8856  lt2sq  8980  le2sq  8981  mulreap  9092
  Copyright terms: Public domain W3C validator