Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > syl6ibr | GIF version |
Description: A mixed syllogism inference from a nested implication and a biconditional. Useful for substituting an embedded consequent with a definition. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
syl6ibr.1 | ⊢ (𝜑 → (𝜓 → 𝜒)) |
syl6ibr.2 | ⊢ (𝜃 ↔ 𝜒) |
Ref | Expression |
---|---|
syl6ibr | ⊢ (𝜑 → (𝜓 → 𝜃)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | syl6ibr.1 | . 2 ⊢ (𝜑 → (𝜓 → 𝜒)) | |
2 | syl6ibr.2 | . . 3 ⊢ (𝜃 ↔ 𝜒) | |
3 | 2 | biimpri 132 | . 2 ⊢ (𝜒 → 𝜃) |
4 | 1, 3 | syl6 33 | 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: 3imtr4g 204 imp4a 346 dcbi 905 oplem1 944 3impexpbicom 1399 hband 1450 hb3and 1451 nfand 1532 nfimd 1549 equsexd 1692 euim 2045 mopick2 2060 2moswapdc 2067 necon3bd 2328 necon3d 2329 necon2ad 2342 necon1abiddc 2347 ralrimd 2487 rspcimedv 2765 2reuswapdc 2861 ra5 2969 difin 3283 r19.2m 3419 r19.2mOLD 3420 tpid3g 3608 sssnm 3651 ssiun 3825 ssiun2 3826 disjnim 3890 exmidsssnc 4096 sotricim 4215 sotritrieq 4217 tron 4274 ordsucss 4390 ordunisuc2r 4400 ordpwsucss 4452 dmcosseq 4780 relssres 4827 trin2 4900 ssrnres 4951 fnun 5199 f1oun 5355 ssimaex 5450 chfnrn 5499 dffo4 5536 dffo5 5537 isoselem 5689 fnoprabg 5840 poxp 6097 issmo2 6154 smores 6157 tfr0dm 6187 tfrlemibxssdm 6192 tfr1onlembxssdm 6208 tfrcllembxssdm 6221 swoer 6425 qsss 6456 findcard 6750 findcard2 6751 findcard2s 6752 supmoti 6848 ctmlemr 6961 ctm 6962 pm54.43 7014 indpi 7118 recexprlemm 7400 recexprlemloc 7407 recexprlem1ssl 7409 recexprlem1ssu 7410 recexprlemss1l 7411 recexprlemss1u 7412 zmulcl 9075 indstr 9356 eluzdc 9372 icoshft 9741 fzouzsplit 9924 hashunlem 10518 modfsummod 11195 dvds2lem 11432 oddnn02np1 11504 dfgcd2 11629 sqrt2irr 11767 ennnfonelemhom 11855 distop 12181 epttop 12186 restdis 12280 cnrest2 12332 cnptopresti 12334 uptx 12370 txcn 12371 decidr 12930 bj-omssind 13060 bj-om 13062 bj-inf2vnlem3 13097 bj-inf2vnlem4 13098 |
Copyright terms: Public domain | W3C validator |