Theorem impancom 258

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 114	. . 3 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	com23 78	. 2 ⊢ (𝜑 → (𝜒 → (𝜓 → 𝜃)))
4	3	imp 123	1 ⊢ ((𝜑 ∧ 𝜒) → (𝜓 → 𝜃))

Syntax hints:   → wi 4   ∧ wa 103

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

This theorem is referenced by:  eqrdav  2163  disjiun  3971  euotd  4226  onsucelsucr  4479  isotr  5778  spc2ed  6192  ltbtwnnqq  7347  genpcdl  7451  genpcuu  7452  un0addcl  9138  un0mulcl  9139  btwnnz  9276  uznfz  10028  elfz0ubfz0  10050  fzoss1  10096  elfzo0z  10109  fzofzim  10113  elfzom1p1elfzo  10139  ssfzo12bi  10150  subfzo0  10167  modfzo0difsn  10320  expaddzap  10489  caucvgre  10909  caubnd2  11045  summodc  11310  fzo0dvdseq  11780  nno  11828  lcmdvds  11990  hashgcdeq  12148  modprm0  12163  pcqcl  12215  neii1  12688  neii2  12690  fsumcncntop  13097