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

Theorem bitr4d 184
Description: Deduction form of bitr4i 180. (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 133 . 2 (𝜑 → (𝜒𝜃))
41, 3bitrd 181 1 (𝜑 → (𝜓𝜃))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 102
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105
This theorem depends on definitions:  df-bi 114
This theorem is referenced by:  3bitr2d  209  3bitr2rd  210  3bitr4d  213  3bitr4rd  214  bianabs  553  imordc  807  3anibar  1083  xor2dc  1297  bilukdc  1303  reuhypd  4230  opelresi  4650  iota1  4908  funbrfv2b  5245  dffn5im  5246  fneqeql  5302  f1ompt  5347  dff13  5434  fliftcnv  5462  isotr  5483  isoini  5484  caovord3  5701  releldm2  5838  tpostpos  5909  nnaordi  6111  iserd  6162  ecdmn0m  6178  qliftel  6216  qliftfun  6218  qliftf  6221  ecopovsym  6232  supisolem  6411  recmulnqg  6546  nqtri3or  6551  ltmnqg  6556  mullocprlem  6725  addextpr  6776  gt0srpr  6890  ltsosr  6906  ltasrg  6912  xrlenlt  7142  letri3  7157  subadd  7276  ltsubadd2  7501  lesubadd2  7503  suble  7508  ltsub23  7510  ltaddpos2  7521  ltsubpos  7522  subge02  7546  ltaddsublt  7635  reapneg  7661  apsym  7670  apti  7686  leltap  7688  ap0gt0  7702  divmulap  7727  divmulap3  7729  rec11rap  7761  ltdiv1  7908  ltdivmul2  7918  ledivmul2  7920  ltrec  7923  nnle1eq1  8013  avgle1  8221  avgle2  8222  nn0le0eq0  8266  znnnlt1  8349  zleltp1  8356  elz2  8369  uzm1  8598  uzin  8600  difrp  8716  xrletri3  8821  xltnegi  8848  elioo5  8902  elfz5  8983  fzdifsuc  9044  elfzm11  9054  uzsplit  9055  elfzonelfzo  9187  qtri3or  9199  qavgle  9214  flqbi  9239  flqbi2  9240  zmodid2  9301  q2submod  9334  sqap0  9485  lt2sq  9492  le2sq  9493  nn0opthlem1d  9587  ibcval5  9630  shftfib  9651  mulreap  9691  caucvgrelemcau  9806  caucvgre  9807  elicc4abs  9920  abs2difabs  9934  cau4  9942  clim2  10034  climeq  10050  dvdsval3  10111  dvdslelemd  10154  dvdsabseq  10158  dvdsflip  10162  dvdsssfz1  10163  zeo3  10178  algcvgblem  10250
  Copyright terms: Public domain W3C validator