Theorem mpan9 516

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 35	. 2 ⊢ (𝜒 → (𝜑 → 𝜃))
4	3	impcom 413	1 ⊢ ((𝜑 ∧ 𝜒) → 𝜃)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  sylan  592  vtocl2gf  3538  vtocl3gf  3539  vtocl2g  3540  vtocl3g  3541  sbcthdv  3762  elinsn  4678  axprlem4OLD  5403  swopolem  5581  wereu  5659  funssres  6584  dffv2  6980  fmptcof  7130  fnprb  7210  fntpb  7211  fliftfuns  7318  isorel  7330  oveqrspc2v  7443  caovclg  7608  caovcomg  7611  caovassg  7614  caovcang  7617  caovordig  7621  caovordg  7623  caovdig  7630  caovdirg  7633  caofidlcan  7718  peano5  7892  dmfexALT  7907  frpoins3xp3g  8139  fvmpocurryd  8269  qliftfuns  8804  nneneq  9193  ttrcltr  9688  ttrclselem2  9698  frins3  9730  cfslb  10261  hsmexlem4  10424  axdc3lem2  10446  axdc4lem  10450  adderpq  10952  mulerpq  10953  ltordlem  11750  lble  12178  uz11  12899  xrsupsslem  13345  xrinfmsslem  13346  xrsupss  13347  xrinfmss  13348  fseqsupubi  14028  hashbclem  14503  ccatass  14640  swrdswrd  14760  swrdccatin1  14780  swrdccatin2  14784  cshwcsh2id  14885  wwlktovf  15013  isercolllem1  15736  caucvgb  15751  zsum  15788  fsum  15790  fsumf1o  15793  fsumcvg2  15797  isummulc2  15832  fsum2dlem  15840  fsumcom2  15844  fsumshftm  15851  fsum0diag2  15853  fsum00  15869  fsumrlim  15882  o1fsum  15884  isumshft  15912  clim2prod  15961  ntrivcvgfvn0  15972  zprod  16010  fprod  16014  fprodf1o  16019  prodss  16020  fprodser  16022  fprodcllemf  16031  fprodm1s  16043  fprodp1s  16044  fprodabs  16047  fprod2dlem  16053  fprodcom2  16057  fprodefsum  16167  mod2eq1n2dvds  16423  sumeven  16463  sumodd  16464  lcmfun  16721  pythagtriplem4  16897  pcmptdvds  16972  prslem  18371  posi  18391  dlatmjdi  18597  lidrididd  18747  grpidinv2  19088  qsxpid  19267  ghmlin  19315  cntzmhm2  19436  dprdss  20125  dprd2d2  20140  omndadd  20222  srgrz  20313  srglz  20314  ringinvnz1ne0  20409  rrgeq0i  20828  lmodlema  21016  islmodd  21017  lsscl  21093  lsslss  21112  lspdisjb  21280  lsslinds  22011  assalem  22037  fvmptnn04if  23036  chfacfscmulgsum  23047  chfacfpmmulgsum  23051  ssnei2  23303  t1ficld  23514  t1sep2  23556  unconn  23616  1stcclb  23631  ptbasfi  23769  tx1stc  23838  qtoptop2  23887  r0sep  23936  ustincl  24396  ustdiag  24397  ustinvel  24398  ustexhalf  24399  psmet0  24496  psmettri2  24497  prdsdsf  24555  prdsxmet  24557  cncfi  25084  ovolfiniun  25691  mbfimaopnlem  25845  limciun  26084  dvcn  26111  dvmptfsum  26165  dvfsumle  26211  dvfsumabs  26213  dvfsumlem3  26218  itgsubst  26239  fsumvma  27408  dchrelbasd  27434  dchrisumlem3  27686  ssslts1  27997  ssslts2  27998  madeval2  28057  elmade  28081  axcontlem9  29353  usgruspgrb  29567  uspgrloopvtxel  29900  umgr2v2evtxel  29906  clwwlknonex2lem2  30502  loop1cycl  30547  3spthd  30574  grpoass  30902  lnolin  31153  elnlfn  32327  strlem4  32653  hstrlem4  32661  atmd  32798  nn0min  33211  slmdlema  33563  esumcvg  34516  measxun2  34641  sibfima  34769  bnj110  35287  bnj594  35341  bnj1491  35486  cvmcov  35768  mrsubcn  36024  dfon2lem5  36290  ifscgr  36549  nn0prpw  36867  neibastop2lem  36904  axnulregtco  37024  tr0el  37029  dfttc4  37074  bj-restb  37769  poimirlem25  38329  poimirlem32  38336  mbfresfi  38350  totbndss  38461  ghomlinOLD  38572  rngodi  38588  rngodir  38589  rngoass  38590  rngohomadd  38653  rngohommul  38654  crngocom  38685  idladdcl  38703  idllmulcl  38704  idlrmulcl  38705  exlimddvf  38803  oposlem  39989  cvlexch1  40135  hlsuprexch  40188  lautle  40891  elrfirn2  43460  wepwsolem  43802  kelac1  43823  islssfg2  43831  lnmlssfg  43840  onov0suclim  44034  relprel  45693  ovolval5lem3  47401  2elfz3nn0  48086  2elfz2melfz  48088  icceuelpartlem  48217  wtgoldbnnsum4prm  48600  bgoldbnnsum3prm  48602  bgoldbtbnd  48607  gpgedg2iv  48865  pgnbgreunbgrlem3  48916  pgnbgreunbgrlem6  48922  oppcendc  49829  setrec2fun  50503