New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > mpbiri | Unicode version |
Description: An inference from a nested biconditional, related to modus ponens. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 25-Oct-2012.) |
Ref | Expression |
---|---|
mpbiri.min | |
mpbiri.maj |
Ref | Expression |
---|---|
mpbiri |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mpbiri.min | . . 3 | |
2 | 1 | a1i 10 | . 2 |
3 | mpbiri.maj | . 2 | |
4 | 2, 3 | mpbird 223 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 wb 176 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-3 7 ax-mp 8 |
This theorem depends on definitions: df-bi 177 |
This theorem is referenced by: dedt 923 nfald2 1972 nfabd2 2507 dedhb 3006 sbceqal 3097 ssdifeq0 3632 r19.2zb 3640 dedth 3703 pwidg 3734 elpr2 3752 snidg 3758 ifpr 3774 prid1g 3825 pwpw0 3855 sssn 3864 pwsnALT 3882 unimax 3925 intmin3 3954 preqr1 4124 el1c 4139 eqpw1 4162 elxpk 4196 opkabssvvk 4208 cokrelk 4284 abexv 4324 eqpw1uni 4330 pw1equn 4331 pw1eqadj 4332 sspw12 4336 iotassuni 4355 0cnsuc 4401 nnc0suc 4412 nnsucelr 4428 nndisjeq 4429 snfi 4431 lefinrflx 4467 lenltfin 4469 ncfinprop 4474 ncfinraise 4481 ncfinlower 4483 tfinltfinlem1 4500 evenodddisj 4516 sfintfin 4532 sfinltfin 4535 vfinspsslem1 4550 vfinspss 4551 proj1op 4600 copsexg 4607 syl6eqbr 4676 elopab 4696 brsi 4761 br1st 4858 br2nd 4859 brswap2 4860 ididg 4871 iss 5000 dmxpss 5052 xpexr 5109 fn0 5202 f00 5249 f1o00 5317 fo00 5318 dffn5 5363 fvopab4t 5385 fsn 5432 fvi 5442 fconstfv 5456 brswap 5509 oprabid 5550 ov6g 5600 ovelrn 5608 caovmo 5645 op1st2nd 5790 txpcofun 5803 mapsspm 6021 mapsspw 6022 map0e 6023 map0 6025 mapsn 6026 en0 6042 xpassen 6057 enprmaplem5 6080 nenpw1pwlem2 6085 elncs 6119 ncseqnc 6128 eqnc2 6129 1cnc 6139 ncdisjeq 6148 peano4nc 6150 2p1e3c 6156 eqtc 6161 ce0addcnnul 6179 ce0nnulb 6182 ncpw1pwneg 6201 sbthlem1 6203 sbth 6206 addlec 6208 nc0le1 6216 leconnnc 6218 addceq0 6219 dflec3 6221 lenc 6223 tc11 6227 taddc 6228 letc 6230 ce0t 6231 ce2le 6232 ce0lenc1 6238 addcdi 6249 muc0or 6251 0lt1c 6257 spacid 6283 nchoicelem9 6295 nchoicelem14 6300 nchoicelem17 6303 nchoicelem19 6305 frecsuc 6320 scancan 6329 |
Copyright terms: Public domain | W3C validator |