![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > mpbii | 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 |
---|---|
mpbii.min |
![]() ![]() |
mpbii.maj |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
mpbii |
![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mpbii.min |
. . 3
![]() ![]() | |
2 | 1 | a1i 9 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() |
3 | mpbii.maj |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 2, 3 | mpbid 146 |
1
![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: pm2.26dc 854 orandc 888 19.9ht 1584 ax11v2 1755 ax11v 1762 ax11ev 1763 equs5or 1765 nfsbxy 1873 nfsbxyt 1874 eqvisset 2643 vtoclgf 2691 vtoclg1f 2692 eueq3dc 2803 mo2icl 2808 csbiegf 2985 un00 3348 sneqr 3626 preqr1 3634 preq12b 3636 prel12 3637 nfopd 3661 ssex 3997 exmidundif 4058 iunpw 4330 nfimad 4816 dfrel2 4915 funsng 5094 cnvresid 5122 nffvd 5352 fnbrfvb 5380 funfvop 5450 acexmidlema 5681 tposf12 6072 supsnti 6780 recidnq 7049 ltaddnq 7063 ltadd1sr 7419 pncan3 7787 divcanap2 8244 ltp1 8402 ltm1 8404 recreclt 8458 nn0ind-raph 8962 2tnp1ge0ge0 9857 fsumcnv 10980 ef01bndlem 11196 sin01gt0 11201 cos01gt0 11202 ltoddhalfle 11320 bezoutlemnewy 11412 bdsepnft 12486 bdssex 12501 bj-inex 12506 bj-d0clsepcl 12528 bj-2inf 12541 bj-inf2vnlem2 12574 |
Copyright terms: Public domain | W3C validator |