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  2569  eqrdav  2739  spc2ed  3614  rexraleqim  3660  disjiun  5154  disjord  5155  disjiund  5157  propeqop  5526  euotd  5532  pwssun  5590  iotan0  6563  funopsn  7182  isotr  7372  funeldmb  7395  funfv1st2nd  8087  funelss  8088  el2mpocsbcl  8126  ressuppssdif  8226  oeordi  8643  domunsncan  9138  pssnn  9234  findcard3  9346  findcard3OLD  9347  ordtypelem7  9593  inf3lem5  9701  r1tr  9845  cardmin2  10068  ac10ct  10103  isf32lem12  10433  isfin1-3  10455  fin17  10463  fin1a2s  10483  axdc4lem  10524  axcclem  10526  ttukeylem2  10579  genpcd  11075  ltexprlem3  11107  prlem936  11116  supsrlem  11180  mul0or  11930  un0addcl  12586  un0mulcl  12587  btwnnz  12719  uznfz  13667  elfz0ubfz0  13689  elfzo0z  13758  fzofzim  13763  ssfzoulel  13810  ssfzo12bi  13811  fzoopth  13812  subfzo0  13839  modmuladdim  13965  modaddmodup  13985  modfzo0difsn  13994  axdc4uzlem  14034  expaddz  14157  sq01  14274  hashnn0n0nn  14440  hashss  14458  hashgt12el  14471  fi1uzind  14556  brfi1indALT  14559  ccatalpha  14641  swrdswrdlem  14752  swrdswrd  14753  swrdccatin1  14773  pfxccatin12lem3  14780  repswswrd  14832  cshf1  14858  cshw1  14870  2cshwcshw  14874  sqrmo  15300  caubnd2  15406  summo  15765  nno  16430  divalglem8  16448  lcmdvds  16655  lcmfunsnlem1  16684  hashgcdeq  16836  modprm0  16852  pcqcl  16903  vdwnnlem3  17044  prmgaplem5  17102  prmgaplem7  17104  catpropd  17767  cicsym  17865  isinitoi  18066  istermoi  18067  iszeroi  18076  acsfiindd  18623  tsrlemax  18656  issubg4  19185  gsmsymgreqlem2  19473  oddvdsnn0  19586  oddvds  19589  gexdvds  19626  lt6abl  19937  pgpfac1lem3  20121  01eq0ring  20556  isphld  21695  psdmul  22193  coe1ae0  22239  mdetdiaglem  22625  slesolex  22709  pmatcoe1fsupp  22728  cpmatelimp  22739  cpmatelimp2  22741  cpmatmcllem  22745  pm2mpf1  22826  mp2pm2mplem4  22836  fvmptnn04ifa  22877  fvmptnn04ifd  22880  chfacfscmul0  22885  chfacfpmmul0  22889  neii1  23135  neii2  23137  uncmp  23432  isfild  23887  fbunfip  23898  fgss2  23903  fgcl  23907  isufil2  23937  cfinufil  23957  ufilen  23959  fsumcn  24913  lmmbr  25311  iscau4  25332  caussi  25350  cmslssbn  25425  ovoliunnul  25561  ovolicc2lem4  25574  itg1ge0a  25766  rolle  26048  ulmcaulem  26455  cxpge0  26743  fsumvma  27275  gausslemma2dlem1a  27427  2sqb  27494  2sq2  27495  pntrsumbnd2  27629  pntlem3  27671  nofv  27720  sltres  27725  muls0ord  28229  axeuclid  28996  axcontlem2  28998  usgrislfuspgr  29222  nbuhgr2vtx1edgblem  29386  usgredgsscusgredg  29495  upgrwlkvtxedg  29681  uspgr2wlkeq  29682  cyclnspth  29836  uspgrn2crct  29841  crctcshwlkn0lem4  29846  wlkiswwlks2lem5  29906  wlknewwlksn  29920  umgrwwlks2on  29990  clwwlkccatlem  30021  clwlkclwwlklem2a4  30029  clwlkclwwlklem2a  30030  clwwisshclwwslemlem  30045  clwwlkel  30078  wwlksubclwwlk  30090  clwwlknon1  30129  clwwlknonex2lem2  30140  uhgr3cyclexlem  30213  vdgn1frgrv3  30329  2wspmdisj  30369  frgrregord013  30427  spansncvi  31684  lnconi  32065  cdj3lem1  32466  metider  33840  prsrcmpltd  35057  gonar  35363  goalr  35365  satffunlem2lem1  35372  finminlem  36284  clsint2  36295  bj-finsumval0  37251  finxpsuclem  37363  pibt2  37383  wl-exeq  37488  phpreu  37564  poimirlem26  37606  poimir  37613  ismtyima  37763  elpaddn0  39757  tendospcanN  40980  nnproddivdvdsd  41957  dvdsexpnn0  42321  rexzrexnn0  42760  unxpwdom3  43052  unielss  43179  onov0suclim  43236  fsovrfovd  43971  radcnvrat  44283  2reu8i  47028  zm1nn  47217  subsubelfzo0  47241  2ffzoeq  47242  fargshiftf  47314  2pwp1prm  47463  lighneal  47485  isuspgrimlem  47758  isassintop  47933  uzlidlring  47958  2zrngamgm  47968  ply1mulgsumlem1  48115  suppdm  48239  rrxsphere  48482  inlinecirc02plem  48520  pgindnf  48808