![]() |
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 635 |
. 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 630 |
This theorem depends on definitions: df-bi 110 |
This theorem is referenced by: jaod 637 jaoa 640 pm2.53 641 pm1.4 646 imorri 668 ioran 669 pm3.14 670 pm1.2 673 orim12i 676 pm1.5 682 pm2.41 693 pm2.42 694 pm2.4 695 pm4.44 696 jaoian 709 pm2.64 714 pm2.76 721 pm2.82 725 pm3.2ni 726 andi 731 condc 749 pm2.61ddc 758 pm5.18dc 777 dcim 784 imorr 797 pm4.78i 808 pm2.85dc 811 peircedc 820 dcan 842 dcor 843 pm4.42r 878 oplem1 882 xoranor 1268 biassdc 1286 anxordi 1291 19.33 1373 hbequid 1406 hbor 1438 19.30dc 1518 19.43 1519 19.32r 1570 hbae 1606 equvini 1641 equveli 1642 exdistrfor 1681 dveeq2 1696 dveeq2or 1697 sbequi 1720 nfsbxy 1818 nfsbxyt 1819 sbcomxyyz 1846 dvelimALT 1886 dvelimfv 1887 dvelimor 1894 modc 1943 mooran1 1972 moexexdc 1984 rgen2a 2375 r19.32r 2457 eueq2dc 2714 eueq3dc 2715 sbcor 2807 sspssr 3043 elun 3084 ssun 3122 inss 3166 undif3ss 3198 elpr2 3397 sssnr 3524 ssprr 3527 sstpr 3528 preq12b 3541 copsexg 3981 sotritric 4061 regexmidlem1 4258 nn0eln0 4341 xpeq0r 4746 funtpg 4950 acexmidlemcase 5507 acexmidlem2 5509 nnm00 6102 renfdisj 7079 nn0ge0 8207 elnnnn0b 8226 elnn0z 8258 nn0n0n1ge2b 8320 nn0ind-raph 8355 uzin 8505 elnn1uz2 8544 indstr2 8546 xrnemnf 8699 xrnepnf 8700 mnfltxr 8707 nn0pnfge0 8712 elfzonlteqm1 9066 fldiv4p1lem1div2 9147 flqeqceilz 9160 m1expcl2 9277 bj-nn0suc 10089 bj-inf2vnlem2 10096 bj-nn0sucALT 10103 |
Copyright terms: Public domain | W3C validator |