Theorem mpan9 514

Description: Modus ponens conjoining dissimilar antecedents. (Contributed by NM, 1-Feb-2008.) (Proof shortened by Andrew Salmon, 7-May-2011.)

Hypotheses

Ref	Expression
mpan9.1	⊢ (𝜑 → 𝜓)
mpan9.2	⊢ (𝜒 → (𝜓 → 𝜃))

Assertion

Ref	Expression
mpan9	⊢ ((𝜑 ∧ 𝜒) → 𝜃)

Proof of Theorem mpan9

Step	Hyp	Ref	Expression
1		mpan9.1	. . 3 ⊢ (𝜑 → 𝜓)
2		mpan9.2	. . 3 ⊢ (𝜒 → (𝜓 → 𝜃))
3	1, 2	syl5 34	. 2 ⊢ (𝜒 → (𝜑 → 𝜃))
4	3	impcom 411	1 ⊢ ((𝜑 ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 399

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 209  df-an 400

This theorem is referenced by:  sylan  589  vtocl2gf  3535  vtocl3gf  3536  vtocl2g  3537  vtocl3g  3538  sbcthdv  3758  elinsn  4666  axprlem4OLD  5384  swopolem  5561  wereu  5639  funssres  6560  dffv2  6957  fmptcof  7107  fnprb  7187  fntpb  7188  fliftfuns  7293  isorel  7305  oveqrspc2v  7418  caovclg  7583  caovcomg  7586  caovassg  7589  caovcang  7592  caovordig  7596  caovordg  7598  caovdig  7605  caovdirg  7608  caofidlcan  7693  peano5  7869  dmfexALT  7884  frpoins3xp3g  8115  fvmpocurryd  8245  qliftfuns  8780  nneneq  9168  ttrcltr  9665  ttrclselem2  9675  frins3  9707  cfslb  10217  hsmexlem4  10380  axdc3lem2  10402  axdc4lem  10406  adderpq  10908  mulerpq  10909  ltordlem  11706  lble  12138  uz11  12858  xrsupsslem  13304  xrinfmsslem  13305  xrsupss  13306  xrinfmss  13307  fseqsupubi  13985  hashbclem  14459  ccatass  14596  swrdswrd  14712  swrdccatin1  14732  swrdccatin2  14736  cshwcsh2id  14835  wwlktovf  14963  isercolllem1  15683  caucvgb  15698  zsum  15736  fsum  15738  fsumf1o  15741  fsumcvg2  15745  isummulc2  15780  fsum2dlem  15788  fsumcom2  15792  fsumshftm  15799  fsum0diag2  15801  fsum00  15817  fsumrlim  15830  o1fsum  15832  isumshft  15860  clim2prod  15909  ntrivcvgfvn0  15920  zprod  15958  fprod  15962  fprodf1o  15967  prodss  15968  fprodser  15970  fprodcllemf  15979  fprodm1s  15991  fprodp1s  15992  fprodabs  15995  fprod2dlem  16001  fprodcom2  16005  fprodefsum  16116  mod2eq1n2dvds  16372  sumeven  16412  lcmfun  16670  pythagtriplem4  16846  pcmptdvds  16921  prslem  18320  posi  18340  dlatmjdi  18546  lidrididd  18695  grpidinv2  19030  ghmlin  19252  cntzmhm2  19373  dprdss  20062  dprd2d2  20077  omndadd  20159  srgrz  20244  srglz  20245  ringinvnz1ne0  20337  rrgeq0i  20736  lmodlema  20920  islmodd  20921  lsscl  20997  lsslss  21016  lspdisjb  21184  lsslinds  21871  assalem  21897  fvmptnn04if  22897  chfacfscmulgsum  22908  chfacfpmmulgsum  22912  ssnei2  23164  t1ficld  23375  t1sep2  23417  unconn  23477  1stcclb  23492  ptbasfi  23629  tx1stc  23698  qtoptop2  23747  r0sep  23796  ustincl  24256  ustdiag  24257  ustinvel  24258  ustexhalf  24259  psmet0  24356  psmettri2  24357  prdsdsf  24415  prdsxmet  24417  cncfi  24944  ovolfiniun  25551  mbfimaopnlem  25705  limciun  25944  dvcn  25971  dvmptfsum  26025  dvfsumle  26071  dvfsumabs  26073  dvfsumlem3  26078  itgsubst  26099  fsumvma  27265  dchrelbasd  27291  dchrisumlem3  27543  ssslts1  27854  ssslts2  27855  madeval2  27914  elmade  27938  axcontlem9  29130  usgruspgrb  29341  uspgrloopvtxel  29674  umgr2v2evtxel  29680  clwwlknonex2lem2  30267  3spthd  30335  grpoass  30663  lnolin  30914  elnlfn  32088  strlem4  32414  hstrlem4  32422  atmd  32559  nn0min  32984  slmdlema  33344  qsxpid  33509  esumcvg  34344  measxun2  34468  sibfima  34596  bnj110  35114  bnj594  35168  bnj1491  35313  loop1cycl  35448  cvmcov  35574  mrsubcn  35830  dfon2lem5  36096  ifscgr  36355  nn0prpw  36644  neibastop2lem  36681  axnulregtco  36801  tr0el  36806  dfttc4  36851  bj-restb  37545  poimirlem25  38105  poimirlem32  38112  mbfresfi  38126  totbndss  38237  ghomlinOLD  38348  rngodi  38364  rngodir  38365  rngoass  38366  rngohomadd  38429  rngohommul  38430  crngocom  38461  idladdcl  38479  idllmulcl  38480  idlrmulcl  38481  exlimddvf  38581  oposlem  39767  cvlexch1  39913  hlsuprexch  39966  lautle  40669  elrfirn2  43238  wepwsolem  43580  kelac1  43601  islssfg2  43609  lnmlssfg  43618  onov0suclim  43812  relprel  45488  ovolval5lem3  47189  2elfz3nn0  47871  2elfz2melfz  47873  icceuelpartlem  48002  wtgoldbnnsum4prm  48385  bgoldbnnsum3prm  48387  bgoldbtbnd  48392  gpgedg2iv  48650  pgnbgreunbgrlem3  48701  pgnbgreunbgrlem6  48707  oppcendc  49600  setrec2fun  50274