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 113 | . 2 ⊢ (𝜑 → (𝜓 → ((𝜒 ∧ 𝜃) → 𝜏))) |
3 | 2 | exp4a 358 | 1 ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏)))) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 102 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 |
This theorem depends on definitions: df-bi 115 |
This theorem is referenced by: exp43 364 reuss2 3244 nndi 6088 mulnqprl 6758 mulnqpru 6759 distrlem5prl 6776 distrlem5pru 6777 recexprlemss1l 6825 recexprlemss1u 6826 lemul12a 7940 nnmulcl 8060 elfz0fzfz0 9137 fzo1fzo0n0 9192 fzofzim 9197 elfzodifsumelfzo 9210 le2sq2 9551 oddprmgt2 10515 |
Copyright terms: Public domain | W3C validator |