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  eqrdav  2736  spc2ed  3557  rexraleqim  3603  disjiun  5088  disjord  5089  disjiund  5091  propeqop  5463  euotd  5469  pwssun  5524  iotan0  6490  funopsn  7103  isotr  7292  funeldmb  7315  resf1extb  7886  funfv1st2nd  8000  funelss  8001  el2mpocsbcl  8037  ressuppssdif  8137  oeordi  8525  domunsncan  9017  pssnn  9105  findcard3  9195  ordtypelem7  9441  inf3lem5  9553  r1tr  9700  cardmin2  9923  ac10ct  9956  isf32lem12  10286  isfin1-3  10308  fin17  10316  fin1a2s  10336  axdc4lem  10377  axcclem  10379  ttukeylem2  10432  genpcd  10929  ltexprlem3  10961  prlem936  10970  supsrlem  11034  mul0or  11789  un0addcl  12446  un0mulcl  12447  btwnnz  12580  uznfz  13538  elfz0ubfz0  13560  elfzo0z  13629  fzofzim  13637  ssfzoulel  13688  ssfzo12bi  13689  fzoopth  13690  subfzo0  13720  modmuladdim  13849  modaddmodup  13869  modfzo0difsn  13878  axdc4uzlem  13918  expaddz  14041  sq01  14160  hashnn0n0nn  14326  hashss  14344  hashgt12el  14357  fi1uzind  14442  brfi1indALT  14445  ccatalpha  14529  swrdswrdlem  14639  swrdswrd  14640  swrdccatin1  14660  pfxccatin12lem3  14667  repswswrd  14719  cshf1  14745  cshw1  14757  2cshwcshw  14760  sqrmo  15186  caubnd2  15293  summo  15652  nno  16321  divalglem8  16339  lcmdvds  16547  lcmfunsnlem1  16576  hashgcdeq  16729  modprm0  16745  pcqcl  16796  vdwnnlem3  16937  prmgaplem5  16995  prmgaplem7  16997  catpropd  17644  cicsym  17740  isinitoi  17935  istermoi  17936  iszeroi  17945  acsfiindd  18488  tsrlemax  18521  issubg4  19087  gsmsymgreqlem2  19372  oddvdsnn0  19485  oddvds  19488  gexdvds  19525  lt6abl  19836  pgpfac1lem3  20020  01eq0ring  20475  isphld  21621  psdmul  22121  coe1ae0  22169  mdetdiaglem  22554  slesolex  22638  pmatcoe1fsupp  22657  cpmatelimp  22668  cpmatelimp2  22670  cpmatmcllem  22674  pm2mpf1  22755  mp2pm2mplem4  22765  fvmptnn04ifa  22806  fvmptnn04ifd  22809  chfacfscmul0  22814  chfacfpmmul0  22818  neii1  23062  neii2  23064  uncmp  23359  isfild  23814  fbunfip  23825  fgss2  23830  fgcl  23834  isufil2  23864  cfinufil  23884  ufilen  23886  fsumcn  24829  lmmbr  25226  iscau4  25247  caussi  25265  cmslssbn  25340  ovoliunnul  25476  ovolicc2lem4  25489  itg1ge0a  25680  rolle  25962  ulmcaulem  26371  cxpge0  26660  fsumvma  27192  gausslemma2dlem1a  27344  2sqb  27411  2sq2  27412  pntrsumbnd2  27546  pntlem3  27588  nofv  27637  ltsres  27642  muls0ord  28193  axeuclid  29048  axcontlem2  29050  usgrislfuspgr  29272  nbuhgr2vtx1edgblem  29436  usgredgsscusgredg  29545  upgrwlkvtxedg  29730  uspgr2wlkeq  29731  cyclnspth  29886  uspgrn2crct  29893  crctcshwlkn0lem4  29898  wlkiswwlks2lem5  29958  wlknewwlksn  29972  usgrwwlks2on  30043  umgrwwlks2on  30044  clwwlkccatlem  30076  clwlkclwwlklem2a4  30084  clwlkclwwlklem2a  30085  clwwisshclwwslemlem  30100  clwwlkel  30133  wwlksubclwwlk  30145  clwwlknon1  30184  clwwlknonex2lem2  30195  uhgr3cyclexlem  30268  vdgn1frgrv3  30384  2wspmdisj  30424  frgrregord013  30482  spansncvi  31739  lnconi  32120  cdj3lem1  32521  constrsqrtcl  33956  metider  34071  prsrcmpltd  35256  onvf1odlem4  35319  gonar  35608  goalr  35610  satffunlem2lem1  35617  finminlem  36531  clsint2  36542  cgsex2gd  37389  bj-finsumval0  37537  finxpsuclem  37649  pibt2  37669  wl-exeq  37786  phpreu  37852  poimirlem26  37894  poimir  37901  ismtyima  38051  elpaddn0  40173  tendospcanN  41396  nnproddivdvdsd  42367  dvdsexpnn0  42701  sn-remul0ord  42775  rexzrexnn0  43158  unxpwdom3  43449  unielss  43572  onov0suclim  43628  fsovrfovd  44362  radcnvrat  44667  2reu8i  47470  zm1nn  47659  subsubelfzo0  47683  2ffzoeq  47684  fargshiftf  47797  2pwp1prm  47946  lighneal  47968  isuspgrimlem  48252  upgrimpths  48266  clnbgr3stgrgrlim  48376  gpgedgvtx0  48418  gpgedgvtx1  48419  isassintop  48567  uzlidlring  48592  2zrngamgm  48602  ply1mulgsumlem1  48743  suppdm  48867  rrxsphere  49105  inlinecirc02plem  49143  pgindnf  50072