Theorem impancom 451

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

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  mo4  2567  spc2ed  3544  rexraleqim  3590  disjiun  5074  disjord  5075  disjiund  5077  propeqop  5455  euotd  5461  pwssun  5516  iotan0  6482  funopsn  7095  isotr  7284  funeldmb  7307  resf1extb  7878  funfv1st2nd  7992  funelss  7993  el2mpocsbcl  8028  ressuppssdif  8128  oeordi  8516  domunsncan  9008  pssnn  9096  findcard3  9186  ordtypelem7  9432  inf3lem5  9544  r1tr  9691  cardmin2  9914  ac10ct  9947  isf32lem12  10277  isfin1-3  10299  fin17  10307  fin1a2s  10327  axdc4lem  10368  axcclem  10370  ttukeylem2  10423  genpcd  10920  ltexprlem3  10952  prlem936  10961  supsrlem  11025  mul0or  11781  un0addcl  12461  un0mulcl  12462  btwnnz  12596  uznfz  13555  elfz0ubfz0  13577  elfzo0z  13647  fzofzim  13655  ssfzoulel  13706  ssfzo12bi  13707  fzoopth  13708  subfzo0  13738  modmuladdim  13867  modaddmodup  13887  modfzo0difsn  13896  axdc4uzlem  13936  expaddz  14059  sq01  14178  hashnn0n0nn  14344  hashss  14362  hashgt12el  14375  fi1uzind  14460  brfi1indALT  14463  ccatalpha  14547  swrdswrdlem  14657  swrdswrd  14658  swrdccatin1  14678  pfxccatin12lem3  14685  repswswrd  14737  cshf1  14763  cshw1  14775  2cshwcshw  14778  sqrmo  15204  caubnd2  15311  summo  15670  nno  16342  divalglem8  16360  lcmdvds  16568  lcmfunsnlem1  16597  hashgcdeq  16751  modprm0  16767  pcqcl  16818  vdwnnlem3  16959  prmgaplem5  17017  prmgaplem7  17019  catpropd  17666  cicsym  17762  isinitoi  17957  istermoi  17958  iszeroi  17967  acsfiindd  18510  tsrlemax  18543  issubg4  19112  gsmsymgreqlem2  19397  oddvdsnn0  19510  oddvds  19513  gexdvds  19550  lt6abl  19861  pgpfac1lem3  20045  01eq0ring  20498  isphld  21644  psdmul  22142  coe1ae0  22190  mdetdiaglem  22573  slesolex  22657  pmatcoe1fsupp  22676  cpmatelimp  22687  cpmatelimp2  22689  cpmatmcllem  22693  pm2mpf1  22774  mp2pm2mplem4  22784  fvmptnn04ifa  22825  fvmptnn04ifd  22828  chfacfscmul0  22833  chfacfpmmul0  22837  neii1  23081  neii2  23083  uncmp  23378  isfild  23833  fbunfip  23844  fgss2  23849  fgcl  23853  isufil2  23883  cfinufil  23903  ufilen  23905  fsumcn  24847  lmmbr  25235  iscau4  25256  caussi  25274  cmslssbn  25349  ovoliunnul  25484  ovolicc2lem4  25497  itg1ge0a  25688  rolle  25967  ulmcaulem  26372  cxpge0  26660  fsumvma  27190  gausslemma2dlem1a  27342  2sqb  27409  2sq2  27410  pntrsumbnd2  27544  pntlem3  27586  nofv  27635  ltsres  27640  muls0ord  28191  axeuclid  29046  axcontlem2  29048  usgrislfuspgr  29270  nbuhgr2vtx1edgblem  29434  usgredgsscusgredg  29543  upgrwlkvtxedg  29728  uspgr2wlkeq  29729  cyclnspth  29884  uspgrn2crct  29891  crctcshwlkn0lem4  29896  wlkiswwlks2lem5  29956  wlknewwlksn  29970  usgrwwlks2on  30041  umgrwwlks2on  30042  clwwlkccatlem  30074  clwlkclwwlklem2a4  30082  clwlkclwwlklem2a  30083  clwwisshclwwslemlem  30098  clwwlkel  30131  wwlksubclwwlk  30143  clwwlknon1  30182  clwwlknonex2lem2  30193  uhgr3cyclexlem  30266  vdgn1frgrv3  30382  2wspmdisj  30422  frgrregord013  30480  spansncvi  31738  lnconi  32119  cdj3lem1  32520  constrsqrtcl  33939  metider  34054  prsrcmpltd  35239  onvf1odlem4  35304  gonar  35593  goalr  35595  satffunlem2lem1  35602  finminlem  36516  clsint2  36527  cgsex2gd  37467  bj-finsumval0  37615  finxpsuclem  37727  pibt2  37747  wl-exeq  37873  phpreu  37939  poimirlem26  37981  poimir  37988  ismtyima  38138  elpaddn0  40260  tendospcanN  41483  nnproddivdvdsd  42453  dvdsexpnn0  42780  sn-remul0ord  42854  rexzrexnn0  43250  unxpwdom3  43541  unielss  43664  onov0suclim  43720  fsovrfovd  44454  radcnvrat  44759  2reu8i  47573  zm1nn  47762  subsubelfzo0  47787  2ffzoeq  47788  nnmul2  47790  fargshiftf  47912  2pwp1prm  48064  lighneal  48086  isuspgrimlem  48383  upgrimpths  48397  clnbgr3stgrgrlim  48507  gpgedgvtx0  48549  gpgedgvtx1  48550  isassintop  48698  uzlidlring  48723  2zrngamgm  48733  ply1mulgsumlem1  48874  suppdm  48998  rrxsphere  49236  inlinecirc02plem  49274  pgindnf  50203