Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > nfan | GIF version |
Description: If 𝑥 is not free in 𝜑 and 𝜓, it is not free in (𝜑 ∧ 𝜓). (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof shortened by Wolf Lammen, 13-Jan-2018.) |
Ref | Expression |
---|---|
nfan.1 | ⊢ Ⅎ𝑥𝜑 |
nfan.2 | ⊢ Ⅎ𝑥𝜓 |
Ref | Expression |
---|---|
nfan | ⊢ Ⅎ𝑥(𝜑 ∧ 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfan.1 | . 2 ⊢ Ⅎ𝑥𝜑 | |
2 | nfan.2 | . . 3 ⊢ Ⅎ𝑥𝜓 | |
3 | 2 | a1i 9 | . 2 ⊢ (𝜑 → Ⅎ𝑥𝜓) |
4 | 1, 3 | nfan1 1496 | 1 ⊢ Ⅎ𝑥(𝜑 ∧ 𝜓) |
Colors of variables: wff set class |
Syntax hints: ∧ wa 102 Ⅎwnf 1389 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 ax-5 1376 ax-gen 1378 ax-4 1440 |
This theorem depends on definitions: df-bi 115 df-nf 1390 |
This theorem is referenced by: nf3an 1498 cbvex2 1838 nfsbxyt 1860 sbcomxyyz 1887 nfsb4t 1931 clelab 2203 nfel 2227 2ralbida 2387 reean 2522 nfrabxy 2534 cbvrexf 2572 cbvreu 2575 cbvrab 2599 ceqsex2 2639 vtocl2gaf 2665 rspce 2696 eqvincf 2720 elrabf 2747 elrab3t 2748 rexab2 2758 morex 2776 reu2 2780 sbc2iegf 2884 rmo2ilem 2903 rmo3 2905 csbiebt 2942 csbie2t 2950 cbvrexcsf 2965 cbvreucsf 2966 cbvrabcsf 2967 nfopd 3587 eluniab 3613 dfnfc2 3619 nfdisjv 3778 nfopab 3846 cbvopab 3849 cbvopab1 3851 cbvopab2 3852 cbvopab1s 3853 mpteq12f 3858 nfmpt 3870 cbvmpt 3872 repizf2 3936 nfpo 4056 nfso 4057 nfwe 4110 onintonm 4261 peano2 4336 nfxp 4389 opeliunxp 4413 nfco 4519 elrnmpt1 4603 nfimad 4697 iota2 4913 dffun4f 4938 nffun 4944 imadif 4999 funimaexglem 5002 nffn 5015 nff 5063 nff1 5110 nffo 5125 nff1o 5144 fun11iun 5167 nffvd 5207 fv3 5218 fmptco 5351 nfiso 5466 cbvriota 5498 riota2df 5508 riota5f 5512 nfoprab 5577 mpt2eq123 5584 nfmpt2 5593 cbvoprab1 5596 cbvoprab2 5597 cbvoprab12 5598 cbvoprab3 5600 cbvmpt2x 5602 ovmpt2dxf 5646 opabex3d 5768 opabex3 5769 dfoprab4f 5839 fmpt2x 5846 spc2ed 5874 cnvoprab 5875 f1od2 5876 nfrecs 5945 tfri3 5976 nffrec 6005 erovlem 6221 nneneq 6343 ac6sfi 6379 nfsup 6405 caucvgsrlemgt1 6971 supinfneg 8683 infsupneg 8684 fimaxre2 10109 nfsum1 10193 nfsum 10194 zsupcllemstep 10341 bezoutlemmain 10387 bezoutlemzz 10391 bezout 10400 bdsepnft 10678 bdsepnfALT 10680 bj-findis 10774 strcollnft 10779 |
Copyright terms: Public domain | W3C validator |