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  2561  eqrdav  2730  spc2ed  3551  rexraleqim  3597  disjiun  5074  disjord  5075  disjiund  5077  propeqop  5442  euotd  5448  pwssun  5503  iotan0  6466  funopsn  7076  isotr  7265  funeldmb  7288  resf1extb  7859  funfv1st2nd  7973  funelss  7974  el2mpocsbcl  8010  ressuppssdif  8110  oeordi  8497  domunsncan  8985  pssnn  9073  findcard3  9162  ordtypelem7  9405  inf3lem5  9517  r1tr  9664  cardmin2  9887  ac10ct  9920  isf32lem12  10250  isfin1-3  10272  fin17  10280  fin1a2s  10300  axdc4lem  10341  axcclem  10343  ttukeylem2  10396  genpcd  10892  ltexprlem3  10924  prlem936  10933  supsrlem  10997  mul0or  11752  un0addcl  12409  un0mulcl  12410  btwnnz  12544  uznfz  13505  elfz0ubfz0  13527  elfzo0z  13596  fzofzim  13604  ssfzoulel  13655  ssfzo12bi  13656  fzoopth  13657  subfzo0  13687  modmuladdim  13816  modaddmodup  13836  modfzo0difsn  13845  axdc4uzlem  13885  expaddz  14008  sq01  14127  hashnn0n0nn  14293  hashss  14311  hashgt12el  14324  fi1uzind  14409  brfi1indALT  14412  ccatalpha  14496  swrdswrdlem  14606  swrdswrd  14607  swrdccatin1  14627  pfxccatin12lem3  14634  repswswrd  14686  cshf1  14712  cshw1  14724  2cshwcshw  14727  sqrmo  15153  caubnd2  15260  summo  15619  nno  16288  divalglem8  16306  lcmdvds  16514  lcmfunsnlem1  16543  hashgcdeq  16696  modprm0  16712  pcqcl  16763  vdwnnlem3  16904  prmgaplem5  16962  prmgaplem7  16964  catpropd  17610  cicsym  17706  isinitoi  17901  istermoi  17902  iszeroi  17911  acsfiindd  18454  tsrlemax  18487  issubg4  19053  gsmsymgreqlem2  19338  oddvdsnn0  19451  oddvds  19454  gexdvds  19491  lt6abl  19802  pgpfac1lem3  19986  01eq0ring  20440  isphld  21586  psdmul  22076  coe1ae0  22124  mdetdiaglem  22508  slesolex  22592  pmatcoe1fsupp  22611  cpmatelimp  22622  cpmatelimp2  22624  cpmatmcllem  22628  pm2mpf1  22709  mp2pm2mplem4  22719  fvmptnn04ifa  22760  fvmptnn04ifd  22763  chfacfscmul0  22768  chfacfpmmul0  22772  neii1  23016  neii2  23018  uncmp  23313  isfild  23768  fbunfip  23779  fgss2  23784  fgcl  23788  isufil2  23818  cfinufil  23838  ufilen  23840  fsumcn  24783  lmmbr  25180  iscau4  25201  caussi  25219  cmslssbn  25294  ovoliunnul  25430  ovolicc2lem4  25443  itg1ge0a  25634  rolle  25916  ulmcaulem  26325  cxpge0  26614  fsumvma  27146  gausslemma2dlem1a  27298  2sqb  27365  2sq2  27366  pntrsumbnd2  27500  pntlem3  27542  nofv  27591  sltres  27596  muls0ord  28119  axeuclid  28936  axcontlem2  28938  usgrislfuspgr  29160  nbuhgr2vtx1edgblem  29324  usgredgsscusgredg  29433  upgrwlkvtxedg  29618  uspgr2wlkeq  29619  cyclnspth  29774  uspgrn2crct  29781  crctcshwlkn0lem4  29786  wlkiswwlks2lem5  29846  wlknewwlksn  29860  umgrwwlks2on  29930  clwwlkccatlem  29961  clwlkclwwlklem2a4  29969  clwlkclwwlklem2a  29970  clwwisshclwwslemlem  29985  clwwlkel  30018  wwlksubclwwlk  30030  clwwlknon1  30069  clwwlknonex2lem2  30080  uhgr3cyclexlem  30153  vdgn1frgrv3  30269  2wspmdisj  30309  frgrregord013  30367  spansncvi  31624  lnconi  32005  cdj3lem1  32406  constrsqrtcl  33784  metider  33899  prsrcmpltd  35085  onvf1odlem4  35142  gonar  35431  goalr  35433  satffunlem2lem1  35440  finminlem  36352  clsint2  36363  bj-finsumval0  37319  finxpsuclem  37431  pibt2  37451  wl-exeq  37568  phpreu  37644  poimirlem26  37686  poimir  37693  ismtyima  37843  elpaddn0  39839  tendospcanN  41062  nnproddivdvdsd  42033  dvdsexpnn0  42367  sn-remul0ord  42441  rexzrexnn0  42837  unxpwdom3  43128  unielss  43251  onov0suclim  43307  fsovrfovd  44042  radcnvrat  44347  2reu8i  47144  zm1nn  47333  subsubelfzo0  47357  2ffzoeq  47358  fargshiftf  47471  2pwp1prm  47620  lighneal  47642  isuspgrimlem  47926  upgrimpths  47940  clnbgr3stgrgrlim  48050  gpgedgvtx0  48092  gpgedgvtx1  48093  isassintop  48241  uzlidlring  48266  2zrngamgm  48276  ply1mulgsumlem1  48418  suppdm  48542  rrxsphere  48780  inlinecirc02plem  48818  pgindnf  49748