![]() |
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 415 | . 2 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → (𝜃 → 𝜏))) |
3 | 2 | expd 415 | 1 ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏)))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 395 |
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 207 df-an 396 |
This theorem is referenced by: exp5j 445 oawordri 8586 oaordex 8594 odi 8615 pssnn 9206 alephval3 10147 dfac2b 10168 axdc4lem 10492 leexp1a 14211 wrdsymb0 14583 coprmproddvds 16696 lmodvsmmulgdi 20911 assamulgscm 21938 2ndcctbss 23478 2pthnloop 29763 wwlksnext 29922 frgrregord013 30423 atcvatlem 32413 umgr2cycllem 35124 exp5g 36285 cdleme48gfv1 40518 cdlemg6e 40604 dihord5apre 41244 dihglblem5apreN 41273 iccpartgt 47351 lmodvsmdi 48223 nn0sumshdiglemB 48469 |
Copyright terms: Public domain | W3C validator |