![]() |
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 115 | . 2 ⊢ (𝜑 → (𝜓 → ((𝜒 ∧ 𝜃) → 𝜏))) |
3 | 2 | exp4a 366 | 1 ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏)))) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 104 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 |
This theorem depends on definitions: df-bi 117 |
This theorem is referenced by: exp43 372 reuss2 3430 nndi 6511 mulnqprl 7597 mulnqpru 7598 distrlem5prl 7615 distrlem5pru 7616 recexprlemss1l 7664 recexprlemss1u 7665 lemul12a 8849 nnmulcl 8970 elfz0fzfz0 10156 fzo1fzo0n0 10213 fzofzim 10218 elfzodifsumelfzo 10231 le2sq2 10627 oddprmgt2 12166 infpnlem1 12391 lmodvsdi 13627 |
Copyright terms: Public domain | W3C validator |