![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > jaoi | GIF 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 668 | . 2 ⊢ (((𝜑 → 𝜓) ∧ (𝜒 → 𝜓)) → ((𝜑 ∨ 𝜒) → 𝜓)) | |
4 | 1, 2, 3 | mp2an 417 | 1 ⊢ ((𝜑 ∨ 𝜒) → 𝜓) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∨ wo 662 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 ax-io 663 |
This theorem depends on definitions: df-bi 115 |
This theorem is referenced by: jaod 670 jaoa 673 pm2.53 674 pm1.4 679 imorri 701 ioran 702 pm3.14 703 pm1.2 706 orim12i 709 pm1.5 715 pm2.41 726 pm2.42 727 pm2.4 728 pm4.44 729 jaoian 742 jao1i 743 pm2.64 748 pm2.76 755 pm2.82 759 pm3.2ni 760 andi 765 condc 785 pm2.61ddc 794 pm5.18dc 813 dcim 820 imorr 833 pm4.78i 844 pm2.85dc 847 peircedc 856 dcan 878 dcor 879 pm4.42r 915 oplem1 919 xoranor 1311 biassdc 1329 anxordi 1334 19.33 1416 hbequid 1449 hbor 1481 19.30dc 1561 19.43 1562 19.32r 1613 hbae 1650 equvini 1685 equveli 1686 exdistrfor 1725 dveeq2 1740 dveeq2or 1741 sbequi 1764 nfsbxy 1863 nfsbxyt 1864 sbcomxyyz 1891 dvelimALT 1931 dvelimfv 1932 dvelimor 1939 modc 1988 mooran1 2017 moexexdc 2029 rgen2a 2425 r19.32r 2509 eueq2dc 2778 eueq3dc 2779 sbcor 2871 elun 3127 ssun 3165 inss 3215 undif3ss 3246 ifsbdc 3388 eqifdc 3407 elpr2 3447 sssnr 3574 ssprr 3577 sstpr 3578 preq12b 3591 copsexg 4038 sotritric 4118 regexmidlem1 4315 nn0eln0 4399 xpeq0r 4811 funtpg 5021 acexmidlemcase 5589 acexmidlem2 5591 nnm00 6221 djuss 6682 eldju2ndl 6684 eldju2ndr 6685 updjud 6694 exmidfodomrlemim 6748 renfdisj 7467 nn0ge0 8608 elnnnn0b 8627 xnn0xr 8651 xnn0nemnf 8657 elnn0z 8673 nn0n0n1ge2b 8736 nn0ind-raph 8773 uzin 8960 elnn1uz2 9003 indstr2 9005 nn0ledivnn 9147 xrnemnf 9157 xrnepnf 9158 mnfltxr 9165 nn0pnfge0 9170 elfzonlteqm1 9524 fldiv4p1lem1div2 9615 flqeqceilz 9628 modfzo0difsn 9705 m1expcl2 9828 m1expeven 9853 facp1 9987 faclbnd3 10000 bcn1 10015 hashinfuni 10034 hashfzp1 10081 mulsucdiv2z 10679 nn0o1gt2 10699 nno 10700 nn0o 10701 dfgcd2 10797 mulgcd 10799 gcdmultiplez 10804 dvdssq 10814 cncongr2 10880 prm2orodd 10902 dfphi2 10990 bj-nn0suc 11216 bj-inf2vnlem2 11223 bj-nn0sucALT 11230 el2oss1o 11244 |
Copyright terms: Public domain | W3C validator |