Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > jaod | Unicode version |
Description: Deduction disjoining the antecedents of two implications. (Contributed by NM, 18-Aug-1994.) (Revised by NM, 4-Apr-2013.) |
Ref | Expression |
---|---|
jaod.1 | |
jaod.2 |
Ref | Expression |
---|---|
jaod |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | jaod.1 | . . . 4 | |
2 | 1 | com12 30 | . . 3 |
3 | jaod.2 | . . . 4 | |
4 | 3 | com12 30 | . . 3 |
5 | 2, 4 | jaoi 706 | . 2 |
6 | 5 | com12 30 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wo 698 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-io 699 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: mpjaod 708 jaao 709 orel2 716 pm2.621 737 mtord 773 jaodan 787 pm2.63 790 pm2.74 797 dedlema 954 dedlemb 955 oplem1 960 opthpr 3735 trsucss 4383 ordsucim 4459 onsucelsucr 4467 0elnn 4578 xpsspw 4698 relop 4736 fununi 5238 poxp 6179 nntri1 6443 nnsseleq 6448 nnmordi 6463 nnaordex 6474 nnm00 6476 swoord2 6510 nneneq 6802 exmidonfinlem 7128 elni2 7234 prubl 7406 distrlem4prl 7504 distrlem4pru 7505 ltxrlt 7943 recexre 8453 remulext1 8474 mulext1 8487 un0addcl 9123 un0mulcl 9124 elnnz 9177 zleloe 9214 zindd 9282 uzsplit 9994 fzm1 10002 expcl2lemap 10431 expnegzap 10453 expaddzap 10463 expmulzap 10465 nn0opthd 10596 facdiv 10612 facwordi 10614 bcpasc 10640 recvguniq 10895 absexpzap 10980 maxabslemval 11108 xrmaxiflemval 11147 sumrbdclem 11274 summodc 11280 zsumdc 11281 prodrbdclem 11468 zproddc 11476 prodssdc 11486 fprodcl2lem 11502 fprodsplitsn 11530 ordvdsmul 11727 gcdaddm 11867 lcmdvds 11955 dvdsprime 11998 prmdvdsexpr 12024 prmfac1 12026 unct 12171 baspartn 12448 reopnap 12938 coseq0q4123 13155 decidin 13371 bj-charfun 13382 bj-nntrans 13526 bj-nnelirr 13528 bj-findis 13554 exmid1stab 13572 triap 13600 |
Copyright terms: Public domain | W3C validator |