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  2230  disjiun  4083  euotd  4347  onsucelsucr  4606  isotr  5957  spc2ed  6398  nninfninc  7322  ltbtwnnqq  7635  genpcdl  7739  genpcuu  7740  un0addcl  9435  un0mulcl  9436  btwnnz  9574  uznfz  10338  elfz0ubfz0  10360  fzoss1  10408  elfzo0z  10424  fzofzim  10428  elfzom1p1elfzo  10460  ssfzo12bi  10471  subfzo0  10489  modfzo0difsn  10658  expaddzap  10846  ccatalpha  11194  swrdswrdlem  11289  swrdswrd  11290  swrdccatin1  11310  pfxccatin12lem3  11317  caucvgre  11546  caubnd2  11682  summodc  11949  fzo0dvdseq  12423  nno  12472  lcmdvds  12656  hashgcdeq  12817  modprm0  12832  pcqcl  12884  issubg4m  13785  01eq0ring  14209  neii1  14877  neii2  14879  fsumcncntop  15297  gausslemma2dlem1a  15793  usgrislfuspgrdom  16047  upgrwlkvtxedg  16221  uspgr2wlkeq  16222  clwwlkccatlem  16257  clwwlknonex2lem2  16295