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  3535  vtocl3gf  3536  vtocl2g  3537  vtocl3g  3538  sbcthdv  3758  elinsn  4672  swopolem  5576  wereu  5654  funssres  6612  dffv2  7011  fmptcof  7163  fnprb  7245  fntpb  7246  fliftfuns  7353  isorel  7365  oveqrspc2v  7478  caovclg  7645  caovcomg  7648  caovassg  7651  caovcang  7654  caovordig  7658  caovordg  7660  caovdig  7667  caovdirg  7670  caofidlcan  7763  peano5  7939  dmfexALT  7954  frpoins3xp3g  8195  fvmpocurryd  8326  qliftfuns  8863  nneneq  9259  ttrcltr  9754  ttrclselem2  9764  frins3  9796  setrec2fun  10010  cfslb  10383  hsmexlem4  10546  axdc3lem2  10568  axdc4lem  10572  adderpq  11080  mulerpq  11081  ltordlem  11881  lble  12309  uz11  13030  xrsupsslem  13477  xrinfmsslem  13478  xrsupss  13479  xrinfmss  13480  fseqsupubi  14161  hashbclem  14638  ccatass  14775  swrdswrd  14896  swrdccatin1  14916  swrdccatin2  14920  cshwcsh2id  15021  wwlktovf  15152  isercolllem1  15876  caucvgb  15891  zsum  15928  fsum  15930  fsumf1o  15933  fsumcvg2  15937  isummulc2  15972  fsum2dlem  15980  fsumcom2  15984  fsumshftm  15991  fsum0diag2  15993  fsum00  16009  fsumrlim  16022  o1fsum  16024  isumshft  16052  clim2prod  16101  ntrivcvgfvn0  16112  zprod  16148  fprod  16152  fprodf1o  16157  prodss  16158  fprodser  16160  fprodcllemf  16169  fprodm1s  16181  fprodp1s  16182  fprodabs  16185  fprod2dlem  16191  fprodcom2  16195  fprodefsum  16305  mod2eq1n2dvds  16561  sumeven  16601  sumodd  16602  lcmfun  16864  pythagtriplem4  17041  pcmptdvds  17116  prslem  18521  posi  18541  dlatmjdi  18747  lidrididd  18901  grpidinv2  19258  qsxpid  19437  ghmlin  19485  cntzmhm2  19607  dprdss  20296  dprd2d2  20311  omndadd  20393  srgrz  20484  srglz  20485  ringinvnz1ne0  20582  rrgeq0i  21002  lmodlema  21191  islmodd  21192  lsscl  21268  lsslss  21287  lspdisjb  21455  lsslinds  22192  assalem  22220  fvmptnn04if  23222  chfacfscmulgsum  23233  chfacfpmmulgsum  23237  ssnei2  23489  t1ficld  23700  t1sep2  23742  unconn  23802  1stcclb  23817  ptbasfi  23955  tx1stc  24024  qtoptop2  24073  r0sep  24122  ustincl  24582  ustdiag  24583  ustinvel  24584  ustexhalf  24585  psmet0  24682  psmettri2  24683  prdsdsf  24741  prdsxmet  24743  cncfi  25270  ovolfiniun  25877  mbfimaopnlem  26031  limciun  26269  dvcn  26296  dvmptfsum  26350  dvfsumle  26396  dvfsumabs  26398  dvfsumlem3  26403  itgsubst  26424  fsumvma  27597  dchrelbasd  27623  dchrisumlem3  27875  ssslts1  28216  ssslts2  28217  madeval2  28276  elmade  28300  axcontlem9  29607  usgruspgrb  29821  uspgrloopvtxel  30154  umgr2v2evtxel  30160  clwwlknonex2lem2  30756  loop1cycl  30801  3spthd  30834  grpoass  31162  lnolin  31413  elnlfn  32587  strlem4  32913  hstrlem4  32921  atmd  33058  nn0min  33508  slmdlema  33863  esumcvg  34829  measxun2  34954  sibfima  35081  bnj110  35599  bnj594  35653  bnj1491  35798  erscottd  35884  dfac16  35887  acwer1prc  35893  jf1o  36052  cvmcov  36236  mrsubcn  36492  dfon2lem5  36764  ifscgr  37024  nn0prpw  37326  neibastop2lem  37363  axnulregtco  37483  tr0el  37488  dfttc4  37533  bj-restb  38285  poimirlem25  38831  poimirlem32  38838  mbfresfi  38852  totbndss  38977  ghomlinOLD  39088  rngodi  39104  rngodir  39105  rngoass  39106  rngohomadd  39169  rngohommul  39170  crngocom  39201  idladdcl  39219  idllmulcl  39220  idlrmulcl  39221  exlimddvf  39319  oposlem  40505  cvlexch1  40651  hlsuprexch  40704  lautle  41407  elrfirn2  43973  wepwsolem  44315  kelac1  44331  islssfg2  44339  lnmlssfg  44348  onov0suclim  44537  relprel  46205  ovolval5lem3  47937  2elfz3nn0  48659  2elfz2melfz  48661  icceuelpartlem  48790  wtgoldbnnsum4prm  49173  bgoldbnnsum3prm  49175  bgoldbtbnd  49180  gpgedg2iv  49438  pgnbgreunbgrlem3  49489  pgnbgreunbgrlem6  49495  oppcendc  50463