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

Theorem 3bitr4g 212
Description: More general version of 3bitr4i 201. Useful for converting definitions in a formula. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
3bitr4g.1 (φ → (ψχ))
3bitr4g.2 (θψ)
3bitr4g.3 (τχ)
Assertion
Ref Expression
3bitr4g (φ → (θτ))

Proof of Theorem 3bitr4g
StepHypRef Expression
1 3bitr4g.2 . . 3 (θψ)
2 3bitr4g.1 . . 3 (φ → (ψχ))
31, 2syl5bb 181 . 2 (φ → (θχ))
4 3bitr4g.3 . 2 (τχ)
53, 4syl6bbr 187 1 (φ → (θτ))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 98
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  bibi1d  222  pm5.32rd  427  orbi1d  692  dcbid  736  pm4.14dc  775  orbididc  846  3orbi123d  1189  3anbi123d  1190  xorbi2d  1253  xorbi1d  1254  nfbidf  1410  drnf1  1599  drnf2  1600  drsb1  1658  sbal2  1876  eubidh  1884  eubid  1885  mobidh  1912  mobid  1913  eqeq1  2024  eqeq2  2027  eleq1  2078  eleq2  2079  nfceqdf  2155  drnfc1  2172  drnfc2  2173  neeq1  2193  neeq2  2194  neleq1  2275  neleq2  2276  ralbida  2294  rexbida  2295  ralbidv2  2302  rexbidv2  2303  r19.21t  2368  r19.23t  2397  reubida  2465  rmobida  2470  raleqf  2475  rexeqf  2476  reueq1f  2477  rmoeq1f  2478  cbvraldva2  2511  cbvrexdva2  2512  dfsbcq  2739  sbcbid  2789  sbcabel  2812  sbnfc2  2879  psseq1  3004  psseq2  3005  ssconb  3049  uneq1  3063  ineq1  3104  difin2  3172  reuun2  3193  reldisj  3244  undif4  3257  disjssun  3258  sbcssg  3305  eltpg  3386  raltpg  3393  rextpg  3394  opeq1  3519  opeq2  3520  intmin4  3613  dfiun2g  3659  iindif2m  3694  iinin2m  3695  breq  3736  breq1  3737  breq2  3738  treq  3830  opthg2  3946  poeq1  4006  soeq1  4022  ordeq  4054  limeq  4059  rabxfrd  4147  iunpw  4157  opthprc  4314  releq  4345  sbcrel  4349  eqrel  4352  eqrelrel  4364  xpiindim  4396  brcnvg  4439  brresg  4543  resieq  4545  xpcanm  4683  xpcan2m  4684  dmsnopg  4715  dfco2a  4744  cnvpom  4783  cnvsom  4784  iotaeq  4798  sniota  4817  sbcfung  4847  fneq1  4909  fneq2  4910  feq1  4952  feq2  4953  feq3  4954  sbcfng  4966  sbcfg  4967  f1eq1  5008  f1eq2  5009  f1eq3  5010  foeq1  5023  foeq2  5024  foeq3  5025  f1oeq1  5038  f1oeq2  5039  f1oeq3  5040  fun11iun  5068  mpteqb  5182  dffo3  5235  fmptco  5251  dff13  5328  f1imaeq  5335  f1imapss  5336  f1eqcocnv  5352  fliftcnv  5356  isoeq1  5362  isoeq2  5363  isoeq3  5364  isoeq4  5365  isoeq5  5366  isocnv2  5373  acexmid  5431  fnotovb  5467  mpt2eq123  5483  ottposg  5788  dmtpos  5789  smoeq  5823  nnacan  5992  nnmcan  5999  ereq1  6020  ereq2  6021  elecg  6051  ereldm  6056  cbvrald  7173
  Copyright terms: Public domain W3C validator