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  2138  disjiun  3924  euotd  4176  onsucelsucr  4424  isotr  5717  spc2ed  6130  ltbtwnnqq  7228  genpcdl  7332  genpcuu  7333  un0addcl  9015  un0mulcl  9016  btwnnz  9150  uznfz  9888  elfz0ubfz0  9907  fzoss1  9953  elfzo0z  9966  fzofzim  9970  elfzom1p1elfzo  9996  ssfzo12bi  10007  subfzo0  10024  modfzo0difsn  10173  expaddzap  10342  caucvgre  10758  caubnd2  10894  summodc  11157  fzo0dvdseq  11560  nno  11608  lcmdvds  11765  hashgcdeq  11909  neii1  12321  neii2  12323  fsumcncntop  12730