Theorem expd 256

Description: Exportation deduction. (Contributed by NM, 20-Aug-1993.)

Hypothesis

Ref	Expression
exp3a.1	⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))

Assertion

Ref	Expression
expd	⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))

Proof of Theorem expd

Step	Hyp	Ref	Expression
1		exp3a.1	. . . 4 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))
2	1	com12 30	. . 3 ⊢ ((𝜓 ∧ 𝜒) → (𝜑 → 𝜃))
3	2	ex 114	. 2 ⊢ (𝜓 → (𝜒 → (𝜑 → 𝜃)))
4	3	com3r 79	1 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))

Syntax hints:   → wi 4   ∧ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 107

This theorem is referenced by:  expdimp  257  pm3.3  259  syland  291  exp32  362  exp4c  365  exp4d  366  exp42  368  exp44  370  exp5c  373  impl  377  mpan2d  424  a2and  547  pm2.6dc  847  3impib  1179  exp5o  1204  biassdc  1373  exbir  1412  expcomd  1417  expdcom  1418  mopick  2077  ralrimivv  2513  mob2  2864  reuind  2889  difin  3313  reupick3  3361  suctr  4343  tfisi  4501  relop  4689  funcnvuni  5192  fnun  5229  mpteqb  5511  funfvima  5649  poxp  6129  nnmass  6383  supisoti  6897  axprecex  7688  ltnsym  7850  nn0lt2  9132  fzind  9166  fnn0ind  9167  btwnz  9170  lbzbi  9408  ledivge1le  9513  elfz0ubfz0  9902  elfzo0z  9961  fzofzim  9965  flqeqceilz  10091  leexp2r  10347  bernneq  10412  cau3lem  10886  climuni  11062  mulcn2  11081  dvdsabseq  11545  ndvdssub  11627  bezoutlemmain  11686  rplpwr  11715  algcvgblem  11730  euclemma  11824  basis2  12215  txcnp  12440  metcnp3  12680