Theorem mpan9 281

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107

This theorem is used by:  sylan  283  vtocl2gf  2885  vtocl3gf  2886  vtoclegft  2897  sbcthdv  3066  disji2  4122  exmid1stab  4345  swopolem  4450  funssres  5420  fvmptssdm  5790  fmptcof  5875  fliftfuns  6004  isorel  6014  oveqrspc2v  6112  caovclg  6242  caovcomg  6245  caovassg  6248  caovcang  6251  caovordig  6255  caovordg  6257  caovdig  6264  caovdirg  6267  qliftfuns  6893  nneneq  7158  supmoti  7333  exmidonfinlem  7545  recexprlemopl  7992  recexprlemopu  7994  cauappcvgprlemladdrl  8024  caucvgsrlemcl  8156  caucvgsrlemfv  8158  caucvgsr  8169  suplocsrlempr  8174  ltordlem  8811  lble  9279  uz11  9954  seq3caopr3  10941  hashfibclem  11296  ccatass  11390  swrdswrd  11491  swrdccatin1  11511  swrdccatin2  11515  climcaucn  12133  sumdc  12140  fsum3  12170  fsumf1o  12173  fsum3cvg2  12177  isummulc2  12209  fsum2dlemstep  12217  fisumcom2  12221  fsumshftm  12228  fisum0diag2  12230  fsum00  12245  isumshft  12273  clim2prod  12322  prodmodclem2  12360  zproddc  12362  fprodseq  12366  fprodf1o  12371  prodssdc  12372  fprodm1s  12384  fprodp1s  12385  fprodcllemf  12396  fprodabs  12399  fprod2dlemstep  12405  fprodcom2fi  12409  dvdsprm  12932  pythagtriplem4  13067  pcmptdvds  13144  lidrididd  13751  grpidinv2  13912  ghmlin  14100  srgrz  14337  srglz  14338  ringinvnz1ne0  14403  rrgeq0i  14621  lmodlema  14677  islmodd  14678  lsslss  14767  assalem  15052  ssnei2  15307  psmet0  15477  psmettri2  15478  cncfi  15728  dvcn  15850  dvmptfsum  15875  usgruspgrben  16525  wlk1walkdom  16698  clwwlknonex2lem2  16777  nninfsellemdc  17151