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  615  imordc  904  ifpnst  996  3anibar  1191  xor2dc  1434  bilukdc  1440  snelpwg  4302  prelpw  4305  reuhypd  4568  opelresi  5024  iota1  5301  funbrfv2b  5690  dffn5im  5691  fneqeql  5755  f1ompt  5798  dff13  5909  fliftcnv  5936  isotr  5957  isoini  5959  caovord3  6196  releldm2  6348  tpostpos  6430  nnsssuc  6670  nnaordi  6676  iserd  6728  ecdmn0m  6746  qliftel  6784  qliftfun  6786  qliftf  6789  ecopovsym  6800  pw2f1odclem  7020  mapen  7032  supisolem  7207  cnvti  7218  omp1eomlem  7293  ctssdc  7312  isomnimap  7336  ismkvmap  7353  iswomnimap  7365  netap  7473  2omotaplemap  7476  recmulnqg  7611  nqtri3or  7616  ltmnqg  7621  mullocprlem  7790  addextpr  7841  gt0srpr  7968  ltsosr  7984  ltasrg  7990  map2psrprg  8025  xrlenlt  8244  letri3  8260  subadd  8382  ltsubadd2  8613  lesubadd2  8615  suble  8620  ltsub23  8622  ltaddpos2  8633  ltsubpos  8634  subge02  8658  ltaddsublt  8751  reapneg  8777  apsym  8786  apti  8802  leltap  8805  ap0gt0  8820  divmulap  8855  divmulap3  8857  rec11rap  8891  ltdiv1  9048  ltdivmul2  9058  ledivmul2  9060  ltrec  9063  suprleubex  9134  nnle1eq1  9167  avgle1  9385  avgle2  9386  nn0le0eq0  9430  znnnlt1  9527  zleltp1  9535  elz2  9551  uzm1  9787  uzin  9789  difrp  9927  xrletri3  10039  xgepnf  10051  xltnegi  10070  xltadd1  10111  xposdif  10117  xleaddadd  10122  elioo5  10168  elfz5  10252  fzdifsuc  10316  elfzm11  10326  uzsplit  10327  elfzonelfzo  10476  qtri3or  10501  qavgle  10519  flqbi  10551  flqbi2  10552  fldiv4lem1div2uz2  10567  zmodid2  10615  q2submod  10648  sqap0  10869  lt2sq  10876  le2sq  10877  nn0opthlem1d  10983  bcval5  11026  zfz1isolemiso  11104  pfxsuffeqwrdeq  11280  shftfib  11385  mulreap  11426  caucvgrelemcau  11542  caucvgre  11543  elicc4abs  11656  abs2difabs  11670  cau4  11678  maxclpr  11784  negfi  11790  lemininf  11796  mul0inf  11803  xrlemininf  11833  xrminltinf  11834  clim2  11845  climeq  11861  fisumss  11955  fsumabs  12028  isumshft  12053  absefib  12334  dvdsval3  12354  dvdslelemd  12406  dvdsabseq  12410  dvdsflip  12414  dvdsssfz1  12415  zeo3  12431  ndvdsadd  12494  bitscmp  12521  dvdssq  12604  algcvgblem  12623  lcmdvds  12653  ncoprmgcdgt1b  12664  isprm3  12692  phiprmpw  12796  prmdiv  12809  pc11  12906  pcz  12907  pockthlem  12931  1arith  12942  ercpbllemg  13415  grpinvcnv  13653  eqger  13813  ablsubadd  13901  dvdsr02  14122  opprunitd  14127  unitsubm  14136  issubrg3  14264  aprval  14299  rnglidlmmgm  14513  znleval2  14671  discld  14863  isneip  14873  restopnb  14908  restopn2  14910  restdis  14911  lmbr2  14941  cnptoprest  14966  cnptoprest2  14967  tx1cn  14996  tx2cn  14997  txcnmpt  15000  txrest  15003  elbl2ps  15119  elbl2  15120  blcomps  15123  blcom  15124  xblpnfps  15125  xblpnf  15126  blpnf  15127  xmeter  15163  bdxmet  15228  metrest  15233  xmetxp  15234  metcn  15241  cncfcdm  15309  reefiso  15504  gausslemma2dlem0c  15783  lgseisenlem3  15804  lgsquadlem1  15809  m1lgs  15817  2lgsoddprmlem2  15838  ausgrusgrben  16022  eupth2lemsfi  16332
  Copyright terms: Public domain W3C validator