![]() |
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 954 dedlemb 955 oplem1 960 opthpr 3731 trsucss 4378 ordsucim 4453 onsucelsucr 4461 0elnn 4572 xpsspw 4691 relop 4729 fununi 5231 poxp 6169 nntri1 6432 nnsseleq 6437 nnmordi 6452 nnaordex 6463 nnm00 6465 swoord2 6499 nneneq 6791 exmidonfinlem 7107 elni2 7213 prubl 7385 distrlem4prl 7483 distrlem4pru 7484 ltxrlt 7922 recexre 8432 remulext1 8453 mulext1 8466 un0addcl 9102 un0mulcl 9103 elnnz 9156 zleloe 9193 zindd 9261 uzsplit 9972 fzm1 9980 expcl2lemap 10409 expnegzap 10431 expaddzap 10441 expmulzap 10443 nn0opthd 10573 facdiv 10589 facwordi 10591 bcpasc 10617 recvguniq 10872 absexpzap 10957 maxabslemval 11085 xrmaxiflemval 11124 sumrbdclem 11251 summodc 11257 zsumdc 11258 prodrbdclem 11445 zproddc 11453 prodssdc 11463 fprodcl2lem 11479 fprodsplitsn 11507 ordvdsmul 11701 gcdaddm 11839 lcmdvds 11927 dvdsprime 11970 prmdvdsexpr 11995 prmfac1 11997 unct 12122 baspartn 12387 reopnap 12877 coseq0q4123 13094 decidin 13309 bj-charfun 13320 bj-nntrans 13464 bj-nnelirr 13466 bj-findis 13492 exmid1stab 13511 triap 13541 |
Copyright terms: Public domain | W3C validator |