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

Theorem bitrd 186
Description: Deduction form of bitri 182. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 14-Apr-2013.)
Hypotheses
Ref Expression
bitrd.1 (𝜑 → (𝜓𝜒))
bitrd.2 (𝜑 → (𝜒𝜃))
Assertion
Ref Expression
bitrd (𝜑 → (𝜓𝜃))

Proof of Theorem bitrd
StepHypRef Expression
1 bitrd.1 . . . 4 (𝜑 → (𝜓𝜒))
21pm5.74i 178 . . 3 ((𝜑𝜓) ↔ (𝜑𝜒))
3 bitrd.2 . . . 4 (𝜑 → (𝜒𝜃))
43pm5.74i 178 . . 3 ((𝜑𝜒) ↔ (𝜑𝜃))
52, 4bitri 182 . 2 ((𝜑𝜓) ↔ (𝜑𝜃))
65pm5.74ri 179 1 (𝜑 → (𝜓𝜃))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 103
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  bitr2d  187  bitr3d  188  bitr4d  189  syl5bb  190  syl6bb  194  3bitrd  212  3bitr2d  214  3bitr3d  216  3bitr4d  218  imbi12d  232  bibi12d  233  sylan9bb  450  anbi12d  457  orbi12d  740  con1biidc  807  pm4.54dc  841  dn1dc  904  dedlem0a  912  xorbi12d  1316  nbbndc  1328  eleq12d  2155  neeq12d  2271  neleq12d  2352  raleqbi1dv  2566  rexeqbi1dv  2567  reueqd  2568  rmoeqd  2569  raleqbidv  2570  rexeqbidv  2571  raleqbidva  2572  rexeqbidva  2573  eueq3dc  2780  sbc19.21g  2896  sbcabel  2909  sbcel1g  2939  sbceq1g  2940  sbcel2g  2941  sbceq2g  2942  sbccsb2g  2949  sbcco3g  2974  sseq12d  3044  raaanlem  3374  sbcssg  3378  ralsng  3468  2ralunsn  3627  csbunig  3646  disjeq12d  3812  breq123d  3836  sbcbr12g  3872  sbcbr1g  3873  sbcbr2g  3874  treq  3919  nalset  3946  copsex4g  4050  sucelon  4295  posng  4480  csbxpg  4489  sbcrel  4494  csbcnvg  4590  eliniseg  4771  brcodir  4788  csbrng  4860  sbcfung  5006  fneq12d  5073  feq12d  5118  feq123d  5119  sbcfng  5126  sbcfg  5127  f1osng  5259  csbfv12g  5305  funimass4  5320  dmfco  5337  eqfnfv  5362  eqfnfv2  5363  fneqeql2  5373  fvimacnvi  5378  funimass3  5380  fniniseg  5384  rexsupp  5388  unpreima  5389  ralrnmpt  5406  rexrnmpt  5407  dffo3  5411  fmptco  5429  fressnfv  5449  eufnfv  5488  foima2  5493  fnunirn  5509  dff13  5510  f1elima  5515  cocan1  5529  cocan2  5530  fliftel  5535  fliftf  5541  isoresbr  5551  isoini  5560  f1oiso  5568  f1ofveu  5603  mpt2eq123dva  5669  ovid  5720  ov  5723  ovg  5742  ovelrn  5752  caovord2d  5773  ofrfval2  5830  offveqb  5833  eqop  5906  reldm  5915  f1od2  5959  mpt2xopoveq  5961  mpt2xopovel  5962  isprmpt2  5964  tpostpos  5985  smoiso  6023  frecabcl  6120  frecsuclem  6127  nnaordr  6223  nnaword  6224  nnaordex  6240  ereq1  6253  brdifun  6273  erth2  6291  qliftfun  6328  brecop  6336  elmapg  6372  elpmg  6375  dom2lem  6443  xpcomco  6496  php5fin  6552  supisolem  6650  inflbti  6666  exmidfodomrlemreseldju  6773  ltapig  6844  ltmpig  6845  nlt1pig  6847  mulcmpblnq  6874  ltsonq  6904  lt2addnq  6910  lt2mulnq  6911  archnqq  6923  prarloclemarch  6924  ltrnqg  6926  mulcmpblnq0  6950  preqlu  6978  genpdflem  7013  addnqprllem  7033  addnqprulem  7034  addlocprlemgt  7040  appdivnq  7069  mulnqprl  7074  mulnqpru  7075  mullocprlem  7076  distrlem4prl  7090  distrlem4pru  7091  1idprl  7096  1idpru  7097  ltexprlemloc  7113  cauappcvgprlemladdrl  7163  cauappcvgprlemladd  7164  cauappcvgprlem1  7165  archrecnq  7169  caucvgprlemnkj  7172  caucvgprprlemexb  7213  addcmpblnr  7232  lttrsr  7255  ltsosr  7257  ltasrg  7263  mulextsr1  7273  srpospr  7275  caucvgsrlemcau  7285  caucvgsrlemgt1  7287  caucvgsrlemoffres  7292  ltresr  7323  axcaucvglemres  7381  cnegexlem1  7604  negeu  7620  subadd2  7633  subcan2  7654  addrsub  7796  ltaddneg  7849  ltaddnegr  7850  ltadd1  7854  leadd2  7856  ltsubadd  7857  lesubadd  7859  ltaddsub2  7862  leaddsub2  7864  ltaddpos  7877  lesub2  7882  ltsub2  7884  ltnegcon1  7888  ltnegcon2  7889  lenegcon1  7891  lenegcon2  7892  addge01  7897  addge02  7898  suble0  7901  leaddle0  7902  lesub0  7904  sublt0d  7991  recexre  7999  reaplt  8009  reapltxor  8010  reapneg  8018  remulext1  8020  apreim  8024  apcotr  8028  apadd2  8030  addext  8031  mulcanap2d  8073  diveqap0  8091  diveqap1  8114  ltmul2  8255  lemul2  8256  ltmulgt11  8263  ltmulgt12  8264  gt0div  8269  ge0div  8270  ltmuldiv  8273  ltrec1  8287  lerec2  8288  ledivdiv  8289  ltdiv23  8291  lediv23  8292  suprleubex  8353  creur  8357  creui  8358  nn1suc  8379  nnrecl  8607  znnsub  8737  zgt0ge1  8744  zltlen  8761  nn0n0n1ge2b  8762  btwnnz  8776  gtndiv  8777  prime  8781  eluz2  8960  indstr2  9031  negm  9035  nn01to3  9037  qapne  9059  qltlen  9060  qreccl  9062  divlt1lt  9136  divle1le  9137  nnledivrp  9172  iccid  9278  elioc2  9289  elico2  9290  elicc2  9291  elfz2  9366  fzen  9392  fzsubel  9408  elfzp1  9419  fzpr  9424  fzrevral2  9453  fzrevral3  9454  nn0disj  9480  2ffzeq  9483  fzosplitsni  9577  fvinim0ffz  9583  ioo0  9602  ico0  9604  ioc0  9605  modq0  9667  negqmod0  9669  zmodidfzo  9691  frecuzrdgtcl  9750  nn0ennn  9771  sq11  9929  nn0le2msqd  10027  nn0opth2d  10031  hashen  10092  zfz1isolem1  10145  zfz1iso  10146  2shfti  10165  cjap  10239  rexfiuz  10321  rexanuz2  10323  abs00ap  10394  absext  10395  sqabs  10414  abslt  10420  absle  10421  absdiflt  10424  absdifle  10425  lenegsq  10427  minmax  10559  ltmininf  10563  clim  10567  clim0c  10572  climrecvg1n  10632  zisum  10668  dvdsval2  10705  zdvdsdc  10723  modmulconst  10734  dvdsaddr  10746  dvdsabseq  10754  fzocongeq  10765  zeo3  10774  odd2np1  10779  oddp1d2  10796  zob  10797  oddm1d2  10798  nnoddm1d2  10816  divalgb  10831  divalgmod  10833  modremain  10835  gcdn0gt0  10875  bezoutlemstep  10892  dvdssq  10926  nn0seqcvgd  10929  algcvgblem  10937  lcmdvds  10967  lcmgcdeq  10971  coprmdvds  10980  qredeq  10984  congr  10988  isprm2  11005  isprm3  11006  prmdvdsexp  11033  prmdvdsexpb  11034  prmexpb  11036  prmfac1  11037  cncongrprm  11042  oddpwdclemxy  11053  oddpwdclemodd  11056  qnumdenbi  11076  qnumgt0  11082  hashdvds  11103  crth  11106  oddennn  11111  cbvrald  11157  bj-nalset  11255  bj-sels  11274  bj-nnelirr  11317
  Copyright terms: Public domain W3C validator