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 419 | . 2 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → (𝜃 → 𝜏))) |
3 | 2 | expd 419 | 1 ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏)))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 399 |
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 210 df-an 400 |
This theorem is referenced by: exp5j 449 oawordri 8220 oaordex 8228 odi 8249 pssnn 8780 pssnnOLD 8828 alephval3 9623 dfac2b 9643 axdc4lem 9968 leexp1a 13644 wrdsymb0 14003 coprmproddvds 16117 lmodvsmmulgdi 19801 assamulgscm 20728 2ndcctbss 22219 2pthnloop 27685 wwlksnext 27844 frgrregord013 28345 atcvatlem 30333 umgr2cycllem 32686 exp5g 34148 cdleme48gfv1 38206 cdlemg6e 38292 dihord5apre 38932 dihglblem5apreN 38961 iccpartgt 44461 lmodvsmdi 45300 nn0sumshdiglemB 45548 |
Copyright terms: Public domain | W3C validator |