![]() |
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 364 | 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 370 reuss2 3361 nndi 6390 mulnqprl 7400 mulnqpru 7401 distrlem5prl 7418 distrlem5pru 7419 recexprlemss1l 7467 recexprlemss1u 7468 lemul12a 8644 nnmulcl 8765 elfz0fzfz0 9934 fzo1fzo0n0 9991 fzofzim 9996 elfzodifsumelfzo 10009 le2sq2 10399 oddprmgt2 11850 |
Copyright terms: Public domain | W3C validator |