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  4028  euotd  4287  onsucelsucr  4544  isotr  5863  spc2ed  6291  nninfninc  7189  ltbtwnnqq  7482  genpcdl  7586  genpcuu  7587  un0addcl  9282  un0mulcl  9283  btwnnz  9420  uznfz  10178  elfz0ubfz0  10200  fzoss1  10247  elfzo0z  10260  fzofzim  10264  elfzom1p1elfzo  10290  ssfzo12bi  10301  subfzo0  10318  modfzo0difsn  10487  expaddzap  10675  caucvgre  11146  caubnd2  11282  summodc  11548  fzo0dvdseq  12022  nno  12071  lcmdvds  12247  hashgcdeq  12408  modprm0  12423  pcqcl  12475  issubg4m  13323  01eq0ring  13745  neii1  14383  neii2  14385  fsumcncntop  14803  gausslemma2dlem1a  15299