Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > jaod | GIF 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 958 dedlemb 959 oplem1 964 opthpr 3746 trsucss 4395 ordsucim 4471 onsucelsucr 4479 0elnn 4590 xpsspw 4710 relop 4748 fununi 5250 poxp 6191 nntri1 6455 nnsseleq 6460 nnmordi 6475 nnaordex 6486 nnm00 6488 swoord2 6522 nneneq 6814 exmidonfinlem 7140 elni2 7246 prubl 7418 distrlem4prl 7516 distrlem4pru 7517 ltxrlt 7955 recexre 8467 remulext1 8488 mulext1 8501 un0addcl 9138 un0mulcl 9139 elnnz 9192 zleloe 9229 zindd 9300 uzsplit 10017 fzm1 10025 expcl2lemap 10457 expnegzap 10479 expaddzap 10489 expmulzap 10491 nn0opthd 10624 facdiv 10640 facwordi 10642 bcpasc 10668 recvguniq 10923 absexpzap 11008 maxabslemval 11136 xrmaxiflemval 11177 sumrbdclem 11304 summodc 11310 zsumdc 11311 prodrbdclem 11498 zproddc 11506 prodssdc 11516 fprodcl2lem 11532 fprodsplitsn 11560 ordvdsmul 11759 gcdaddm 11902 lcmdvds 11990 dvdsprime 12033 prmdvdsexpr 12061 prmfac1 12063 pythagtriplem2 12177 unct 12318 baspartn 12595 reopnap 13085 coseq0q4123 13302 decidin 13519 bj-charfun 13530 bj-nntrans 13674 bj-nnelirr 13676 bj-findis 13702 exmid1stab 13721 triap 13749 |
Copyright terms: Public domain | W3C validator |