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  2566  eqrdav  2735  spc2ed  3555  rexraleqim  3601  disjiun  5086  disjord  5087  disjiund  5089  propeqop  5455  euotd  5461  pwssun  5516  iotan0  6482  funopsn  7093  isotr  7282  funeldmb  7305  resf1extb  7876  funfv1st2nd  7990  funelss  7991  el2mpocsbcl  8027  ressuppssdif  8127  oeordi  8515  domunsncan  9005  pssnn  9093  findcard3  9183  ordtypelem7  9429  inf3lem5  9541  r1tr  9688  cardmin2  9911  ac10ct  9944  isf32lem12  10274  isfin1-3  10296  fin17  10304  fin1a2s  10324  axdc4lem  10365  axcclem  10367  ttukeylem2  10420  genpcd  10917  ltexprlem3  10949  prlem936  10958  supsrlem  11022  mul0or  11777  un0addcl  12434  un0mulcl  12435  btwnnz  12568  uznfz  13526  elfz0ubfz0  13548  elfzo0z  13617  fzofzim  13625  ssfzoulel  13676  ssfzo12bi  13677  fzoopth  13678  subfzo0  13708  modmuladdim  13837  modaddmodup  13857  modfzo0difsn  13866  axdc4uzlem  13906  expaddz  14029  sq01  14148  hashnn0n0nn  14314  hashss  14332  hashgt12el  14345  fi1uzind  14430  brfi1indALT  14433  ccatalpha  14517  swrdswrdlem  14627  swrdswrd  14628  swrdccatin1  14648  pfxccatin12lem3  14655  repswswrd  14707  cshf1  14733  cshw1  14745  2cshwcshw  14748  sqrmo  15174  caubnd2  15281  summo  15640  nno  16309  divalglem8  16327  lcmdvds  16535  lcmfunsnlem1  16564  hashgcdeq  16717  modprm0  16733  pcqcl  16784  vdwnnlem3  16925  prmgaplem5  16983  prmgaplem7  16985  catpropd  17632  cicsym  17728  isinitoi  17923  istermoi  17924  iszeroi  17933  acsfiindd  18476  tsrlemax  18509  issubg4  19075  gsmsymgreqlem2  19360  oddvdsnn0  19473  oddvds  19476  gexdvds  19513  lt6abl  19824  pgpfac1lem3  20008  01eq0ring  20463  isphld  21609  psdmul  22109  coe1ae0  22157  mdetdiaglem  22542  slesolex  22626  pmatcoe1fsupp  22645  cpmatelimp  22656  cpmatelimp2  22658  cpmatmcllem  22662  pm2mpf1  22743  mp2pm2mplem4  22753  fvmptnn04ifa  22794  fvmptnn04ifd  22797  chfacfscmul0  22802  chfacfpmmul0  22806  neii1  23050  neii2  23052  uncmp  23347  isfild  23802  fbunfip  23813  fgss2  23818  fgcl  23822  isufil2  23852  cfinufil  23872  ufilen  23874  fsumcn  24817  lmmbr  25214  iscau4  25235  caussi  25253  cmslssbn  25328  ovoliunnul  25464  ovolicc2lem4  25477  itg1ge0a  25668  rolle  25950  ulmcaulem  26359  cxpge0  26648  fsumvma  27180  gausslemma2dlem1a  27332  2sqb  27399  2sq2  27400  pntrsumbnd2  27534  pntlem3  27576  nofv  27625  ltsres  27630  muls0ord  28181  axeuclid  29036  axcontlem2  29038  usgrislfuspgr  29260  nbuhgr2vtx1edgblem  29424  usgredgsscusgredg  29533  upgrwlkvtxedg  29718  uspgr2wlkeq  29719  cyclnspth  29874  uspgrn2crct  29881  crctcshwlkn0lem4  29886  wlkiswwlks2lem5  29946  wlknewwlksn  29960  usgrwwlks2on  30031  umgrwwlks2on  30032  clwwlkccatlem  30064  clwlkclwwlklem2a4  30072  clwlkclwwlklem2a  30073  clwwisshclwwslemlem  30088  clwwlkel  30121  wwlksubclwwlk  30133  clwwlknon1  30172  clwwlknonex2lem2  30183  uhgr3cyclexlem  30256  vdgn1frgrv3  30372  2wspmdisj  30412  frgrregord013  30470  spansncvi  31727  lnconi  32108  cdj3lem1  32509  constrsqrtcl  33936  metider  34051  prsrcmpltd  35237  onvf1odlem4  35300  gonar  35589  goalr  35591  satffunlem2lem1  35598  finminlem  36512  clsint2  36523  bj-finsumval0  37490  finxpsuclem  37602  pibt2  37622  wl-exeq  37739  phpreu  37805  poimirlem26  37847  poimir  37854  ismtyima  38004  elpaddn0  40060  tendospcanN  41283  nnproddivdvdsd  42254  dvdsexpnn0  42589  sn-remul0ord  42663  rexzrexnn0  43046  unxpwdom3  43337  unielss  43460  onov0suclim  43516  fsovrfovd  44250  radcnvrat  44555  2reu8i  47359  zm1nn  47548  subsubelfzo0  47572  2ffzoeq  47573  fargshiftf  47686  2pwp1prm  47835  lighneal  47857  isuspgrimlem  48141  upgrimpths  48155  clnbgr3stgrgrlim  48265  gpgedgvtx0  48307  gpgedgvtx1  48308  isassintop  48456  uzlidlring  48481  2zrngamgm  48491  ply1mulgsumlem1  48632  suppdm  48756  rrxsphere  48994  inlinecirc02plem  49032  pgindnf  49961