Theorem impancom 445

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

Syntax hints:   → wi 4   ∧ wa 386

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 199  df-an 387

This theorem is referenced by:  eqrdav  2776  rexraleqim  3530  disjiun  4874  disjord  4875  disjiund  4877  propeqop  5204  euotd  5210  pwssun  5257  funopsn  6679  isotr  6858  el2mpt2csbcl  7530  ressuppssdif  7597  oeordi  7951  domunsncan  8348  pssnn  8466  findcard3  8491  ordtypelem7  8718  inf3lem5  8826  r1tr  8936  cardmin2  9157  ac10ct  9190  isf32lem12  9521  isfin1-3  9543  fin17  9551  fin1a2s  9571  axdc4lem  9612  axcclem  9614  ttukeylem2  9667  genpcd  10163  ltexprlem3  10195  prlem936  10204  supsrlem  10268  mul0or  11015  fiminre  11326  un0addcl  11677  un0mulcl  11678  btwnnz  11805  uznfz  12741  elfz0ubfz0  12762  elfzo0z  12829  fzofzim  12834  elfzom1p1elfzo  12867  ssfzoulel  12881  ssfzo12bi  12882  subfzo0  12909  modmuladdim  13032  modaddmodup  13052  modfzo0difsn  13061  axdc4uzlem  13101  expaddz  13222  sq01  13305  hashnn0n0nn  13495  hashss  13511  hashgt12el  13524  fi1uzind  13593  brfi1indALT  13596  ccatalpha  13683  swrdswrdlem  13813  swrdswrd  13814  swrdccatin1  13851  swrdccatin12lem3  13860  repswswrd  13930  cshf1  13961  cshw1  13973  2cshwcshw  13976  sqrmo  14399  caubnd2  14504  summo  14855  nno  15512  divalglem8  15530  lcmdvds  15727  lcmfunsnlem1  15756  hashgcdeq  15898  modprm0  15914  pcqcl  15965  vdwnnlem3  16105  prmgaplem5  16163  prmgaplem7  16165  catpropd  16754  cicsym  16849  isinitoi  17038  istermoi  17039  iszeroi  17044  acsfiindd  17563  tsrlemax  17606  issubg4  17997  gsmsymgreqlem2  18234  oddvdsnn0  18347  oddvds  18350  gexdvds  18383  lt6abl  18682  pgpfac1lem3  18863  coe1ae0  19982  isphld  20397  mdetdiaglem  20809  slesolex  20894  pmatcoe1fsupp  20913  cpmatelimp  20924  cpmatelimp2  20926  cpmatmcllem  20930  pm2mpf1  21011  mp2pm2mplem4  21021  fvmptnn04ifa  21062  fvmptnn04ifd  21065  chfacfscmul0  21070  chfacfpmmul0  21074  neii1  21318  neii2  21320  uncmp  21615  isfild  22070  fbunfip  22081  fgss2  22086  fgcl  22090  isufil2  22120  cfinufil  22140  ufilen  22142  fsumcn  23081  lmmbr  23464  iscau4  23485  caussi  23503  cmslssbn  23578  ovoliunnul  23711  ovolicc2lem4  23724  itg1ge0a  23915  rolle  24190  ulmcaulem  24585  cxpge0  24866  fsumvma  25390  gausslemma2dlem1a  25542  2sqb  25609  pntrsumbnd2  25708  pntlem3  25750  axeuclid  26312  axcontlem2  26314  usgrislfuspgr  26533  nbuhgr2vtx1edgblem  26698  usgredgsscusgredg  26807  upgrwlkvtxedg  26992  uspgr2wlkeq  26993  cyclnspth  27152  uspgrn2crct  27157  crctcshwlkn0lem4  27162  wlkiswwlks2lem5  27222  wlknewwlksn  27237  wlkwwlksurOLD  27248  umgrwwlks2on  27337  clwwlkccatlem  27369  clwwlkccat  27370  clwlkclwwlklem2a4  27377  clwlkclwwlklem2a  27378  clwwisshclwwslemlem  27402  clwwlkel  27437  wwlksubclwwlk  27455  wwlksubclwwlkOLD  27456  clwwlknon1  27499  clwwlknonex2lem2  27510  uhgr3cyclexlem  27584  vdgn1frgrv3  27705  2wspmdisj  27745  frgrregord013  27827  spansncvi  29083  lnconi  29464  cdj3lem1  29865  spc2ed  29884  metider  30535  funeldmb  32254  nofv  32399  sltres  32404  finminlem  32901  clsint2  32912  bj-finsumval0  33749  finxpsuclem  33829  wl-exeq  33915  phpreu  34002  poimirlem26  34045  poimir  34052  ismtyima  34210  elpaddn0  35938  tendospcanN  37161  rexzrexnn0  38310  unxpwdom3  38606  fsovrfovd  39241  radcnvrat  39451  2reu8i  42136  zm1nn  42326  subsubelfzo0  42350  fzoopth  42351  2ffzoeq  42352  fargshiftf  42390  2pwp1prm  42506  lighneal  42531  isomuspgrlem1  42722  isassintop  42843  uzlidlring  42926  2zrngamgm  42936  ply1mulgsumlem1  43171  suppdm  43297  rrxsphere  43466  inlinecirc02plem  43504