Theorem impancom 260

Description: Mixed importation/commutation inference. (Contributed by NM, 22-Jun-2013.)

Hypothesis

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

Assertion

Ref	Expression
impancom	⊢ ((𝜑 ∧ 𝜒) → (𝜓 → 𝜃))

Proof of Theorem impancom

Step	Hyp	Ref	Expression
1		impancom.1	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))
2	1	ex 115	. . 3 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	com23 78	. 2 ⊢ (𝜑 → (𝜒 → (𝜓 → 𝜃)))
4	3	imp 124	1 ⊢ ((𝜑 ∧ 𝜒) → (𝜓 → 𝜃))

Syntax hints:   → wi 4   ∧ wa 104

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

This theorem is referenced by:  eqrdav  2195  disjiun  4029  euotd  4288  onsucelsucr  4545  isotr  5866  spc2ed  6300  nninfninc  7198  ltbtwnnqq  7501  genpcdl  7605  genpcuu  7606  un0addcl  9301  un0mulcl  9302  btwnnz  9439  uznfz  10197  elfz0ubfz0  10219  fzoss1  10266  elfzo0z  10279  fzofzim  10283  elfzom1p1elfzo  10309  ssfzo12bi  10320  subfzo0  10337  modfzo0difsn  10506  expaddzap  10694  caucvgre  11165  caubnd2  11301  summodc  11567  fzo0dvdseq  12041  nno  12090  lcmdvds  12274  hashgcdeq  12435  modprm0  12450  pcqcl  12502  issubg4m  13401  01eq0ring  13823  neii1  14491  neii2  14493  fsumcncntop  14911  gausslemma2dlem1a  15407