![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > jaoi | Unicode version |
Description: Inference disjoining the antecedents of two implications. (Contributed by NM, 5-Apr-1994.) (Revised by NM, 31-Jan-2015.) |
Ref | Expression |
---|---|
jaoi.1 |
![]() ![]() ![]() ![]() ![]() ![]() |
jaoi.2 |
![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
jaoi |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | jaoi.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() | |
2 | jaoi.2 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() | |
3 | pm3.44 634 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 1, 2, 3 | mp2an 402 |
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 99 ax-ia2 100 ax-ia3 101 ax-io 629 |
This theorem depends on definitions: df-bi 110 |
This theorem is referenced by: jaod 636 jaoa 639 pm2.53 640 pm1.4 645 imorri 667 ioran 668 pm3.14 669 pm1.2 672 orim12i 675 pm1.5 681 pm2.41 692 pm2.42 693 pm2.4 694 pm4.44 695 jaoian 708 pm2.64 713 pm2.76 720 pm2.82 724 pm3.2ni 725 andi 730 condc 748 pm2.61ddc 757 pm5.18dc 776 dcim 783 imorr 796 pm4.78i 807 pm2.85dc 810 peircedc 819 dcan 841 dcor 842 pm4.42r 877 oplem1 881 xoranor 1267 biassdc 1283 anxordi 1288 19.33 1370 hbequid 1403 hbor 1435 19.30dc 1515 19.43 1516 19.32r 1567 hbae 1603 equvini 1638 equveli 1639 exdistrfor 1678 dveeq2 1693 dveeq2or 1694 sbequi 1717 nfsbxy 1815 nfsbxyt 1816 sbcomxyyz 1843 dvelimALT 1883 dvelimfv 1884 dvelimor 1891 modc 1940 mooran1 1969 moexexdc 1981 rgen2a 2369 r19.32r 2451 eueq2dc 2708 eueq3dc 2709 sbcor 2801 sspssr 3037 elun 3078 ssun 3116 inss 3160 undif3ss 3192 elpr2 3386 sssnr 3515 ssprr 3518 sstpr 3519 preq12b 3532 copsexg 3972 sotritric 4052 regexmidlem1 4218 nn0eln0 4284 xpeq0r 4689 funtpg 4893 acexmidlemcase 5450 acexmidlem2 5452 nnm00 6038 renfdisj 6876 nn0ge0 7983 elnnnn0b 8002 elnn0z 8034 nn0n0n1ge2b 8096 nn0ind-raph 8131 uzin 8281 elnn1uz2 8320 indstr2 8322 xrnemnf 8469 xrnepnf 8470 mnfltxr 8477 nn0pnfge0 8482 elfzonlteqm1 8836 m1expcl2 8931 bj-nn0suc 9424 bj-inf2vnlem2 9431 bj-nn0sucALT 9438 |
Copyright terms: Public domain | W3C validator |