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

Theorem bitr4d 190
Description: Deduction form of bitr4i 186. (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 140 . 2 (𝜑 → (𝜒𝜃))
41, 3bitrd 187 1 (𝜑 → (𝜓𝜃))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 104
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
This theorem is referenced by:  3bitr2d  215  3bitr2rd  216  3bitr4d  219  3bitr4rd  220  mpbirand  437  mpbiran2d  438  bianabs  600  imordc  882  3anibar  1149  xor2dc  1368  bilukdc  1374  reuhypd  4392  opelresi  4830  iota1  5102  funbrfv2b  5466  dffn5im  5467  fneqeql  5528  f1ompt  5571  dff13  5669  fliftcnv  5696  isotr  5717  isoini  5719  caovord3  5944  releldm2  6083  tpostpos  6161  nnsssuc  6398  nnaordi  6404  iserd  6455  ecdmn0m  6471  qliftel  6509  qliftfun  6511  qliftf  6514  ecopovsym  6525  mapen  6740  supisolem  6895  cnvti  6906  omp1eomlem  6979  ctssdc  6998  isomnimap  7009  ismkvmap  7028  iswomnimap  7038  recmulnqg  7211  nqtri3or  7216  ltmnqg  7221  mullocprlem  7390  addextpr  7441  gt0srpr  7568  ltsosr  7584  ltasrg  7590  map2psrprg  7625  xrlenlt  7841  letri3  7857  subadd  7977  ltsubadd2  8207  lesubadd2  8209  suble  8214  ltsub23  8216  ltaddpos2  8227  ltsubpos  8228  subge02  8252  ltaddsublt  8345  reapneg  8371  apsym  8380  apti  8396  leltap  8399  ap0gt0  8414  divmulap  8447  divmulap3  8449  rec11rap  8483  ltdiv1  8638  ltdivmul2  8648  ledivmul2  8650  ltrec  8653  suprleubex  8724  nnle1eq1  8756  avgle1  8972  avgle2  8973  nn0le0eq0  9017  znnnlt1  9114  zleltp1  9121  elz2  9134  uzm1  9368  uzin  9370  difrp  9492  xrletri3  9600  xgepnf  9611  xltnegi  9630  xltadd1  9671  xposdif  9677  xleaddadd  9682  elioo5  9728  elfz5  9810  fzdifsuc  9873  elfzm11  9883  uzsplit  9884  elfzonelfzo  10019  qtri3or  10032  qavgle  10048  flqbi  10075  flqbi2  10076  zmodid2  10137  q2submod  10170  sqap0  10371  lt2sq  10378  le2sq  10379  nn0opthlem1d  10478  bcval5  10521  zfz1isolemiso  10594  shftfib  10607  mulreap  10648  caucvgrelemcau  10764  caucvgre  10765  elicc4abs  10878  abs2difabs  10892  cau4  10900  maxclpr  11006  negfi  11011  lemininf  11017  mul0inf  11024  xrlemininf  11052  xrminltinf  11053  clim2  11064  climeq  11080  fisumss  11173  fsumabs  11246  isumshft  11271  absefib  11488  dvdsval3  11508  dvdslelemd  11552  dvdsabseq  11556  dvdsflip  11560  dvdsssfz1  11561  zeo3  11576  ndvdsadd  11639  dvdssq  11730  algcvgblem  11741  lcmdvds  11771  ncoprmgcdgt1b  11782  isprm3  11810  phiprmpw  11909  discld  12319  isneip  12329  restopnb  12364  restopn2  12366  restdis  12367  lmbr2  12397  cnptoprest  12422  cnptoprest2  12423  tx1cn  12452  tx2cn  12453  txcnmpt  12456  txrest  12459  elbl2ps  12575  elbl2  12576  blcomps  12579  blcom  12580  xblpnfps  12581  xblpnf  12582  blpnf  12583  xmeter  12619  bdxmet  12684  metrest  12689  xmetxp  12690  metcn  12697  cncffvrn  12752  reefiso  12881
  Copyright terms: Public domain W3C validator