exp4b - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > exp4b		Structured version Visualization version GIF version

Theorem exp4b 430

Description: An exportation inference. (Contributed by NM, 26-Apr-1994.) (Proof shortened by Wolf Lammen, 23-Nov-2012.) Shorten exp4a 431. (Revised by Wolf Lammen, 20-Jul-2021.)

**Hypothesis**
Ref	Expression
exp4b.1	⊢ ((𝜑 ∧ 𝜓) → ((𝜒 ∧ 𝜃) → 𝜏))

**Assertion**
Ref	Expression
exp4b	⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))

**Proof of Theorem exp4b**
Step	Hyp	Ref	Expression
1		exp4b.1	. . 3 ⊢ ((𝜑 ∧ 𝜓) → ((𝜒 ∧ 𝜃) → 𝜏))
2	1	expd 415	. 2 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → (𝜃 → 𝜏)))
3	2	ex 412	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 206 df-an 396

This theorem is referenced by: exp4a 431 exp43 436 somo 5627 tz7.7 6395 f1oweALT 7976 soseq 8164 onfununi 8362 odi 8600 omeu 8606 nndi 8644 inf3lem2 9653 axdc3lem2 10475 genpnmax 11031 mulclprlem 11043 distrlem5pr 11051 reclem4pr 11074 lemul12a 12103 sup2 12201 nnmulcl 12267 zbtwnre 12961 elfz0fzfz0 13639 fzofzim 13712 fzo1fzo0n0 13716 elincfzoext 13723 elfzodifsumelfzo 13731 le2sq2 14132 expnbnd 14227 swrdswrd 14688 swrdccat3blem 14722 climbdd 15651 dvdslegcd 16479 oddprmgt2 16670 unbenlem 16877 infpnlem1 16879 prmgaplem6 17025 lmodvsdi 20768 lspsolvlem 21030 lbsextlem2 21047 gsummoncoe1 22227 cpmatmcllem 22633 mp2pm2mplem4 22724 1stccnp 23379 itg2le 25682 ewlkle 29432 clwlkclwwlklem2a 29821 3vfriswmgr 30101 frgrwopreg 30146 frgr2wwlk1 30152 frgrreg 30217 spansneleq 31393 elspansn4 31396 cvmdi 32147 atcvat3i 32219 mdsymlem3 32228 slmdvsdi 32935 satfv0 34968 satffunlem1lem1 35012 satffunlem2lem1 35014 mclsppslem 35193 dfon2lem8 35386 heicant 37128 areacirclem1 37181 areacirclem2 37182 areacirclem4 37184 areacirc 37186 fzmul 37214 cvlexch1 38800 hlrelat2 38876 cvrat3 38915 snatpsubN 39223 pmaple 39234 sn-sup2 42024 fzopredsuc 46703 gbegt5 47101

W3C validator

	
		OSZAR »