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-mp 5 ax-1 6 ax-2 7 ax-3 8 |
This theorem depends on definitions: df-bi 177 |
This theorem is referenced by: dedt 923 nfald2 1972 nfabd2 2508 dedhb 3007 sbceqal 3098 ssdifeq0 3633 r19.2zb 3641 dedth 3704 pwidg 3735 elpr2 3753 snidg 3759 ifpr 3775 prid1g 3826 pwpw0 3856 sssn 3865 pwsnALT 3883 unimax 3926 intmin3 3955 preqr1 4125 el1c 4140 eqpw1 4163 elxpk 4197 opkabssvvk 4209 cokrelk 4285 abexv 4325 eqpw1uni 4331 pw1equn 4332 pw1eqadj 4333 sspw12 4337 iotassuni 4356 0cnsuc 4402 nnc0suc 4413 nnsucelr 4429 nndisjeq 4430 snfi 4432 lefinrflx 4468 lenltfin 4470 ncfinprop 4475 ncfinraise 4482 ncfinlower 4484 tfinltfinlem1 4501 evenodddisj 4517 sfintfin 4533 sfinltfin 4536 vfinspsslem1 4551 vfinspss 4552 proj1op 4601 copsexg 4608 syl6eqbr 4677 elopab 4697 brsi 4762 br1st 4859 br2nd 4860 brswap2 4861 ididg 4872 iss 5001 dmxpss 5053 xpexr 5110 fn0 5203 f00 5250 f1o00 5318 fo00 5319 dffn5 5364 fvopab4t 5386 fsn 5433 fvi 5443 fconstfv 5457 brswap 5510 oprabid 5551 ov6g 5601 ovelrn 5609 caovmo 5646 op1st2nd 5791 txpcofun 5804 mapsspm 6022 mapsspw 6023 map0e 6024 map0 6026 mapsn 6027 en0 6043 xpassen 6058 enprmaplem5 6081 nenpw1pwlem2 6086 elncs 6120 ncseqnc 6129 eqnc2 6130 1cnc 6140 ncdisjeq 6149 peano4nc 6151 2p1e3c 6157 eqtc 6162 ce0addcnnul 6180 ce0nnulb 6183 ncpw1pwneg 6202 sbthlem1 6204 sbth 6207 addlec 6209 nc0le1 6217 leconnnc 6219 addceq0 6220 dflec3 6222 lenc 6224 tc11 6229 taddc 6230 letc 6232 ce0t 6233 ce2le 6234 ce0lenc1 6240 addcdi 6251 muc0or 6253 0lt1c 6259 spacid 6286 nchoicelem9 6298 nchoicelem14 6303 nchoicelem17 6306 nchoicelem19 6308 frecsuc 6323 scancan 6332 |
Copyright terms: Public domain | W3C validator |