Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > exp4b | GIF version |
Description: An exportation inference. (Contributed by NM, 26-Apr-1994.) (Proof shortened by Wolf Lammen, 23-Nov-2012.) |
Ref | Expression |
---|---|
exp4b.1 | ⊢ ((𝜑 ∧ 𝜓) → ((𝜒 ∧ 𝜃) → 𝜏)) |
Ref | Expression |
---|---|
exp4b | ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏)))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | exp4b.1 | . . 3 ⊢ ((𝜑 ∧ 𝜓) → ((𝜒 ∧ 𝜃) → 𝜏)) | |
2 | 1 | ex 114 | . 2 ⊢ (𝜑 → (𝜓 → ((𝜒 ∧ 𝜃) → 𝜏))) |
3 | 2 | exp4a 363 | 1 ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏)))) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: exp43 369 reuss2 3356 nndi 6382 mulnqprl 7383 mulnqpru 7384 distrlem5prl 7401 distrlem5pru 7402 recexprlemss1l 7450 recexprlemss1u 7451 lemul12a 8627 nnmulcl 8748 elfz0fzfz0 9910 fzo1fzo0n0 9967 fzofzim 9972 elfzodifsumelfzo 9985 le2sq2 10375 oddprmgt2 11821 |
Copyright terms: Public domain | W3C validator |