![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > exp4c | Structured version Visualization version GIF version |
Description: An exportation inference. (Contributed by NM, 26-Apr-1994.) |
Ref | Expression |
---|---|
exp4c.1 | ⊢ (𝜑 → (((𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜏)) |
Ref | Expression |
---|---|
exp4c | ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏)))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | exp4c.1 | . . 3 ⊢ (𝜑 → (((𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜏)) | |
2 | 1 | expd 416 | . 2 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → (𝜃 → 𝜏))) |
3 | 2 | expd 416 | 1 ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏)))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
This theorem depends on definitions: df-bi 208 df-an 397 |
This theorem is referenced by: exp5j 446 oawordri 8017 oaordex 8025 odi 8046 pssnn 8572 alephval3 9371 dfac2b 9391 axdc4lem 9712 leexp1a 13377 wrdsymb0 13735 coprmproddvds 15824 lmodvsmmulgdi 19347 assamulgscm 19806 2ndcctbss 21735 2pthnloop 27187 wwlksnext 27346 frgrregord013 27854 atcvatlem 29841 umgr2cycllem 31951 exp5g 33205 cdleme48gfv1 37153 cdlemg6e 37239 dihord5apre 37879 dihglblem5apreN 37908 iccpartgt 43023 lmodvsmdi 43864 nn0sumshdiglemB 44115 |
Copyright terms: Public domain | W3C validator |