Theorem mpan9 506

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 407	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:  sylan  580  vtocl2gf  3523  vtocl3gf  3524  vtocl2g  3525  vtocl3g  3526  sbcthdv  3752  elinsn  4658  axprlem4OLD  5362  swopolem  5529  wereu  5607  funssres  6520  dffv2  6912  fmptcof  7058  fnprb  7137  fntpb  7138  fliftfuns  7243  isorel  7255  oveqrspc2v  7368  caovclg  7533  caovcomg  7536  caovassg  7539  caovcang  7542  caovordig  7546  caovordg  7548  caovdig  7555  caovdirg  7558  caofidlcan  7643  peano5  7818  dmfexALT  7833  frpoins3xp3g  8066  fvmpocurryd  8196  qliftfuns  8723  nneneq  9110  ttrcltr  9601  ttrclselem2  9611  frins3  9643  cfslb  10152  hsmexlem4  10315  axdc3lem2  10337  axdc4lem  10341  adderpq  10842  mulerpq  10843  ltordlem  11637  lble  12069  uz11  12752  xrsupsslem  13201  xrinfmsslem  13202  xrsupss  13203  xrinfmss  13204  fseqsupubi  13880  hashbclem  14354  ccatass  14491  swrdswrd  14607  swrdccatin1  14627  swrdccatin2  14631  cshwcsh2id  14730  wwlktovf  14858  isercolllem1  15567  caucvgb  15582  zsum  15620  fsum  15622  fsumf1o  15625  fsumcvg2  15629  isummulc2  15664  fsum2dlem  15672  fsumcom2  15676  fsumshftm  15683  fsum0diag2  15685  fsum00  15700  fsumrlim  15713  o1fsum  15715  isumshft  15741  clim2prod  15790  ntrivcvgfvn0  15801  zprod  15839  fprod  15843  fprodf1o  15848  prodss  15849  fprodser  15851  fprodcllemf  15860  fprodm1s  15872  fprodp1s  15873  fprodabs  15876  fprod2dlem  15882  fprodcom2  15886  fprodefsum  15997  mod2eq1n2dvds  16253  sumeven  16293  lcmfun  16551  pythagtriplem4  16726  pcmptdvds  16801  prslem  18198  posi  18218  dlatmjdi  18424  lidrididd  18573  grpidinv2  18905  ghmlin  19128  cntzmhm2  19249  dprdss  19938  dprd2d2  19953  omndadd  20035  srgrz  20120  srglz  20121  ringinvnz1ne0  20213  rrgeq0i  20609  lmodlema  20793  islmodd  20794  lsscl  20870  lsslss  20889  lspdisjb  21058  lsslinds  21763  assalem  21789  fvmptnn04if  22759  chfacfscmulgsum  22770  chfacfpmmulgsum  22774  ssnei2  23026  t1ficld  23237  t1sep2  23279  unconn  23339  1stcclb  23354  ptbasfi  23491  tx1stc  23560  qtoptop2  23609  r0sep  23658  ustincl  24118  ustdiag  24119  ustinvel  24120  ustexhalf  24121  psmet0  24218  psmettri2  24219  prdsdsf  24277  prdsxmet  24279  cncfi  24809  ovolfiniun  25424  mbfimaopnlem  25578  limciun  25817  dvcn  25845  dvmptfsum  25901  dvfsumle  25948  dvfsumleOLD  25949  dvfsumabs  25951  dvfsumlem3  25957  itgsubst  25978  fsumvma  27146  dchrelbasd  27172  dchrisumlem3  27424  sssslt1  27731  sssslt2  27732  madeval2  27789  elmade  27807  axcontlem9  28945  usgruspgrb  29156  uspgrloopvtxel  29490  umgr2v2evtxel  29496  clwwlknonex2lem2  30080  3spthd  30148  grpoass  30475  lnolin  30726  elnlfn  31900  strlem4  32226  hstrlem4  32234  atmd  32371  nn0min  32795  slmdlema  33164  qsxpid  33319  esumcvg  34091  measxun2  34215  sibfima  34343  bnj110  34862  bnj594  34916  bnj1491  35061  loop1cycl  35173  cvmcov  35299  mrsubcn  35555  dfon2lem5  35821  ifscgr  36078  nn0prpw  36357  neibastop2lem  36394  bj-restb  37128  poimirlem25  37685  poimirlem32  37692  mbfresfi  37706  totbndss  37817  ghomlinOLD  37928  rngodi  37944  rngodir  37945  rngoass  37946  rngohomadd  38009  rngohommul  38010  crngocom  38041  idladdcl  38059  idllmulcl  38060  idlrmulcl  38061  exlimddvf  38161  oposlem  39221  cvlexch1  39367  hlsuprexch  39420  lautle  40123  elrfirn2  42729  wepwsolem  43075  kelac1  43096  islssfg2  43104  lnmlssfg  43113  onov0suclim  43307  relprel  44984  ovolval5lem3  46692  2elfz3nn0  47347  2elfz2melfz  47349  icceuelpartlem  47466  wtgoldbnnsum4prm  47833  bgoldbnnsum3prm  47835  bgoldbtbnd  47840  gpgedg2iv  48098  pgnbgreunbgrlem3  48149  pgnbgreunbgrlem6  48155  oppcendc  49050  setrec2fun  49724