![]() |
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 206 df-an 397 |
This theorem is referenced by: exp5j 446 oawordri 8535 oaordex 8543 odi 8564 pssnn 9153 pssnnOLD 9250 alephval3 10089 dfac2b 10109 axdc4lem 10434 leexp1a 14124 wrdsymb0 14483 coprmproddvds 16584 lmodvsmmulgdi 20458 assamulgscm 21388 2ndcctbss 22890 2pthnloop 28917 wwlksnext 29076 frgrregord013 29577 atcvatlem 31565 umgr2cycllem 34026 exp5g 35056 cdleme48gfv1 39276 cdlemg6e 39362 dihord5apre 40002 dihglblem5apreN 40031 iccpartgt 45931 lmodvsmdi 46770 nn0sumshdiglemB 47018 |
Copyright terms: Public domain | W3C validator |