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

Theorem bitr4d 191
Description: Deduction form of bitr4i 187. (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 141 . 2 (𝜑 → (𝜒𝜃))
41, 3bitrd 188 1 (𝜑 → (𝜓𝜃))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 105
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
This theorem is referenced by:  3bitr2d  216  3bitr2rd  217  3bitr4d  220  3bitr4rd  221  mpbirand  441  mpbiran2d  442  bianabs  611  imordc  897  3anibar  1165  xor2dc  1390  bilukdc  1396  reuhypd  4465  opelresi  4911  iota1  5184  funbrfv2b  5552  dffn5im  5553  fneqeql  5616  f1ompt  5659  dff13  5759  fliftcnv  5786  isotr  5807  isoini  5809  caovord3  6038  releldm2  6176  tpostpos  6255  nnsssuc  6493  nnaordi  6499  iserd  6551  ecdmn0m  6567  qliftel  6605  qliftfun  6607  qliftf  6610  ecopovsym  6621  mapen  6836  supisolem  6997  cnvti  7008  omp1eomlem  7083  ctssdc  7102  isomnimap  7125  ismkvmap  7142  iswomnimap  7154  recmulnqg  7365  nqtri3or  7370  ltmnqg  7375  mullocprlem  7544  addextpr  7595  gt0srpr  7722  ltsosr  7738  ltasrg  7744  map2psrprg  7779  xrlenlt  7996  letri3  8012  subadd  8134  ltsubadd2  8364  lesubadd2  8366  suble  8371  ltsub23  8373  ltaddpos2  8384  ltsubpos  8385  subge02  8409  ltaddsublt  8502  reapneg  8528  apsym  8537  apti  8553  leltap  8556  ap0gt0  8571  divmulap  8604  divmulap3  8606  rec11rap  8640  ltdiv1  8796  ltdivmul2  8806  ledivmul2  8808  ltrec  8811  suprleubex  8882  nnle1eq1  8914  avgle1  9130  avgle2  9131  nn0le0eq0  9175  znnnlt1  9272  zleltp1  9279  elz2  9295  uzm1  9529  uzin  9531  difrp  9661  xrletri3  9773  xgepnf  9785  xltnegi  9804  xltadd1  9845  xposdif  9851  xleaddadd  9856  elioo5  9902  elfz5  9985  fzdifsuc  10049  elfzm11  10059  uzsplit  10060  elfzonelfzo  10198  qtri3or  10211  qavgle  10227  flqbi  10258  flqbi2  10259  zmodid2  10320  q2submod  10353  sqap0  10554  lt2sq  10561  le2sq  10562  nn0opthlem1d  10666  bcval5  10709  zfz1isolemiso  10786  shftfib  10799  mulreap  10840  caucvgrelemcau  10956  caucvgre  10957  elicc4abs  11070  abs2difabs  11084  cau4  11092  maxclpr  11198  negfi  11203  lemininf  11209  mul0inf  11216  xrlemininf  11246  xrminltinf  11247  clim2  11258  climeq  11274  fisumss  11367  fsumabs  11440  isumshft  11465  absefib  11745  dvdsval3  11765  dvdslelemd  11815  dvdsabseq  11819  dvdsflip  11823  dvdsssfz1  11824  zeo3  11839  ndvdsadd  11902  dvdssq  11998  algcvgblem  12015  lcmdvds  12045  ncoprmgcdgt1b  12056  isprm3  12084  phiprmpw  12188  prmdiv  12201  pc11  12296  pcz  12297  pockthlem  12320  1arith  12331  grpinvcnv  12797  ablsubadd  12911  discld  13129  isneip  13139  restopnb  13174  restopn2  13176  restdis  13177  lmbr2  13207  cnptoprest  13232  cnptoprest2  13233  tx1cn  13262  tx2cn  13263  txcnmpt  13266  txrest  13269  elbl2ps  13385  elbl2  13386  blcomps  13389  blcom  13390  xblpnfps  13391  xblpnf  13392  blpnf  13393  xmeter  13429  bdxmet  13494  metrest  13499  xmetxp  13500  metcn  13507  cncffvrn  13562  reefiso  13691
  Copyright terms: Public domain W3C validator